Three

📁 Source: Mathlib/CategoryTheory/ComposableArrows/Three.lean

Statistics

Metric	Count
Definitions threeδ₁Toδ₀, threeδ₁Toδ₀', threeδ₂Toδ₁, threeδ₂Toδ₁', threeδ₃Toδ₂, threeδ₃Toδ₂'	6
Theorems threeδ₁Toδ₀_app_one, threeδ₁Toδ₀_app_two, threeδ₁Toδ₀_app_zero, threeδ₂Toδ₁_app_one, threeδ₂Toδ₁_app_two, threeδ₂Toδ₁_app_zero, threeδ₃Toδ₂_app_one, threeδ₃Toδ₂_app_two, threeδ₃Toδ₂_app_zero	9
Total	15

CategoryTheory.ComposableArrows

Definitions

Name	Category	Theorems
threeδ₁Toδ₀ 📖	CompOp	3 math math: threeδ₁Toδ₀_app_zero, threeδ₁Toδ₀_app_two, threeδ₁Toδ₀_app_one
threeδ₁Toδ₀' 📖	CompOp	—
threeδ₂Toδ₁ 📖	CompOp	3 math math: threeδ₂Toδ₁_app_zero, threeδ₂Toδ₁_app_one, threeδ₂Toδ₁_app_two
threeδ₂Toδ₁' 📖	CompOp	—
threeδ₃Toδ₂ 📖	CompOp	3 math math: threeδ₃Toδ₂_app_one, threeδ₃Toδ₂_app_two, threeδ₃Toδ₂_app_zero
threeδ₃Toδ₂' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
threeδ₁Toδ₀_app_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₂ threeδ₁Toδ₀ CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj	—	—
threeδ₁Toδ₀_app_two 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₂ threeδ₁Toδ₀ CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj	—	—
threeδ₁Toδ₀_app_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₂ threeδ₁Toδ₀	—	—
threeδ₂Toδ₁_app_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₂ threeδ₂Toδ₁	—	—
threeδ₂Toδ₁_app_two 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₂ threeδ₂Toδ₁ CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj	—	—
threeδ₂Toδ₁_app_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₂ threeδ₂Toδ₁ CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj	—	—
threeδ₃Toδ₂_app_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₂ threeδ₃Toδ₂ CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj	—	—
threeδ₃Toδ₂_app_two 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₂ threeδ₃Toδ₂	—	—
threeδ₃Toδ₂_app_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₂ threeδ₃Toδ₂ CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj	—	—

---

← Back to Index