Four

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

Statistics

Metric	Count
Definitions fourδ₁Toδ₀, fourδ₁Toδ₀', fourδ₂Toδ₁, fourδ₂Toδ₁', fourδ₃Toδ₂, fourδ₃Toδ₂', fourδ₄Toδ₃, fourδ₄Toδ₃'	8
Theorems fourδ₁Toδ₀_app_one, fourδ₁Toδ₀_app_three, fourδ₁Toδ₀_app_two, fourδ₁Toδ₀_app_zero, fourδ₂Toδ₁_app_one, fourδ₂Toδ₁_app_three, fourδ₂Toδ₁_app_two, fourδ₂Toδ₁_app_zero, fourδ₃Toδ₂_app_one, fourδ₃Toδ₂_app_three, fourδ₃Toδ₂_app_two, fourδ₃Toδ₂_app_zero, fourδ₄Toδ₃_app_one, fourδ₄Toδ₃_app_three, fourδ₄Toδ₃_app_two, fourδ₄Toδ₃_app_zero	16
Total	24

CategoryTheory.ComposableArrows

Definitions

Name	Category	Theorems
fourδ₁Toδ₀ 📖	CompOp	4 math math: fourδ₁Toδ₀_app_zero, fourδ₁Toδ₀_app_two, fourδ₁Toδ₀_app_one, fourδ₁Toδ₀_app_three
fourδ₁Toδ₀' 📖	CompOp	—
fourδ₂Toδ₁ 📖	CompOp	4 math math: fourδ₂Toδ₁_app_three, fourδ₂Toδ₁_app_zero, fourδ₂Toδ₁_app_one, fourδ₂Toδ₁_app_two
fourδ₂Toδ₁' 📖	CompOp	—
fourδ₃Toδ₂ 📖	CompOp	4 math math: fourδ₃Toδ₂_app_one, fourδ₃Toδ₂_app_two, fourδ₃Toδ₂_app_three, fourδ₃Toδ₂_app_zero
fourδ₃Toδ₂' 📖	CompOp	—
fourδ₄Toδ₃ 📖	CompOp	4 math math: fourδ₄Toδ₃_app_two, fourδ₄Toδ₃_app_one, fourδ₄Toδ₃_app_zero, fourδ₄Toδ₃_app_three
fourδ₄Toδ₃' 📖	CompOp	—

Theorems

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

---

← Back to Index