Documentation Verification Report

ToMkOne

📁 Source: Mathlib/AlgebraicTopology/SimplexCategory/ToMkOne.lean

Statistics

Metric	Count
Definitions `toMk₁`, `toMk₁Equiv`	2
Theorems `toMk₁Equiv_apply`, `toMk₁_apply`, `toMk₁_apply_eq_one_iff`, `toMk₁_apply_eq_zero_iff`, `toMk₁_bijective`, `toMk₁_injective`, `toMk₁_of_castSucc_lt`, `toMk₁_of_le_castSucc`, `toMk₁_surjective`, `δ_comp_toMk₁_of_le`, `δ_comp_toMk₁_of_lt`, `σ_comp_toMk₁_of_le`, `σ_comp_toMk₁_of_lt`	13
Total	15

SimplexCategory

Definitions

Name	Category	Theorems
`toMk₁` 📖	CompOp	13 math math: `toMk₁_apply_eq_zero_iff`, `toMk₁Equiv_apply`, `toMk₁_of_le_castSucc`, `toMk₁_apply`, `σ_comp_toMk₁_of_lt`, `δ_comp_toMk₁_of_le`, `toMk₁_of_castSucc_lt`, `toMk₁_surjective`, `toMk₁_bijective`, `σ_comp_toMk₁_of_le`, `toMk₁_apply_eq_one_iff`, `δ_comp_toMk₁_of_lt`, `toMk₁_injective`
`toMk₁Equiv` 📖	CompOp	1 math math: `toMk₁Equiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMk₁Equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `SimplexCategory` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `EquivLike.toFunLike` `Equiv.instEquivLike` `toMk₁Equiv` `toMk₁`	—	—
`toMk₁_apply` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `len` `Fin.instPartialOrder` `CategoryTheory.ConcreteCategory.hom` `SimplexCategory` `smallCategory` `OrderHom.instFunLike` `instConcreteCategoryOrderHomFinHAddNatLenOfNat` `toMk₁` `instOfNatToTypeOrderHomFinHAddNatLenOfNat`	—	—
`toMk₁_apply_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `len` `Fin.instPartialOrder` `CategoryTheory.ConcreteCategory.hom` `SimplexCategory` `smallCategory` `OrderHom.instFunLike` `instConcreteCategoryOrderHomFinHAddNatLenOfNat` `toMk₁` `instOfNatToTypeOrderHomFinHAddNatLenOfNat`	—	—
`toMk₁_apply_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `len` `Fin.instPartialOrder` `CategoryTheory.ConcreteCategory.hom` `SimplexCategory` `smallCategory` `OrderHom.instFunLike` `instConcreteCategoryOrderHomFinHAddNatLenOfNat` `toMk₁` `instOfNatToTypeOrderHomFinHAddNatLenOfNat`	—	—
`toMk₁_bijective` 📖	mathematical	—	`Function.Bijective` `Quiver.Hom` `SimplexCategory` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `toMk₁`	—	`toMk₁_injective` `toMk₁_surjective`
`toMk₁_injective` 📖	mathematical	—	`Quiver.Hom` `SimplexCategory` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `toMk₁`	—	`lt_of_lt_of_le` `CategoryTheory.ConcreteCategory.congr_hom`
`toMk₁_of_castSucc_lt` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `len` `Fin.instPartialOrder` `CategoryTheory.ConcreteCategory.hom` `SimplexCategory` `smallCategory` `OrderHom.instFunLike` `instConcreteCategoryOrderHomFinHAddNatLenOfNat` `toMk₁` `instOfNatToTypeOrderHomFinHAddNatLenOfNat`	—	—
`toMk₁_of_le_castSucc` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `len` `Fin.instPartialOrder` `CategoryTheory.ConcreteCategory.hom` `SimplexCategory` `smallCategory` `OrderHom.instFunLike` `instConcreteCategoryOrderHomFinHAddNatLenOfNat` `toMk₁` `instOfNatToTypeOrderHomFinHAddNatLenOfNat`	—	—
`toMk₁_surjective` 📖	mathematical	—	`Quiver.Hom` `SimplexCategory` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `toMk₁`	—	`CategoryTheory.ConcreteCategory.hom_ext` `Finset.min'_le` `Fintype.complete`
`δ_comp_toMk₁_of_le` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `toMk₁` `Fin.castPred` `Fin.ne_last_of_lt` `lt_of_le_of_lt` `PartialOrder.toPreorder` `Fin.instPartialOrder`	—	`Fin.ne_last_of_lt` `lt_of_le_of_lt` `Fin.eq_castSucc_of_ne_last` `Iff.not` `LT.lt.ne` `Fin.castPred_castSucc` `CategoryTheory.ConcreteCategory.hom_ext` `Fin.eq_iff_eq_zero_iff` `toMk₁_apply_eq_zero_iff`
`δ_comp_toMk₁_of_lt` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `toMk₁` `Fin.ne_zero_of_lt`	—	`Fin.ne_zero_of_lt` `CategoryTheory.ConcreteCategory.hom_ext` `Fin.eq_iff_eq_zero_iff` `toMk₁_apply_eq_zero_iff`
`σ_comp_toMk₁_of_le` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `σ` `toMk₁`	—	`CategoryTheory.ConcreteCategory.hom_ext` `toMk₁_of_le_castSucc` `Fin.predAbove_of_le_castSucc` `Fin.castSucc_castPred`
`σ_comp_toMk₁_of_lt` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `σ` `toMk₁`	—	`CategoryTheory.ConcreteCategory.hom_ext` `toMk₁_of_castSucc_lt` `Fin.ne_zero_of_lt` `Fin.predAbove_of_castSucc_lt` `Fin.castSucc_pred_lt_iff` `Fin.predAbove_of_le_castSucc` `lt_of_le_of_lt` `Fin.castSucc_castPred`

---

← Back to Index