Alpha

📁 Source: SDG/IsKockLawvere_one/Alpha.lean

Statistics

Metric	Count
Definitions α	1
Theorems bijective_α, injective_α, surjective_α, α_apply	4
Total	5

SDG

Definitions

Name	Category	Theorems
α 📖	CompOp	4 math math: surjective_α, α_apply, injective_α, bijective_α

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_α 📖	mathematical	—	D α	—	injective_α surjective_α
injective_α 📖	mathematical	—	D α	—	α_apply cancel_d
surjective_α 📖	mathematical	—	D α	—	IsKockLawvere_one.isKockLawvere_one α_apply
α_apply 📖	mathematical	—	D α	—	—

---

← Back to Index