Documentation Verification Report

StdSimplexOne

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/StdSimplexOne.lean

Statistics

Metric	Count
Definitions `objMk₁`	1
Theorems `objMk₁_apply`, `objMk₁_apply_eq_one_iff`, `objMk₁_apply_eq_zero_iff`, `objMk₁_bijective`, `objMk₁_injective`, `objMk₁_of_castSucc_lt`, `objMk₁_of_le_castSucc`, `objMk₁_surjective`, `δ_objMk₁_of_le`, `δ_objMk₁_of_lt`, `σ_objMk₁_of_le`, `σ_objMk₁_of_lt`	12
Total	13

SSet.stdSimplex

Definitions

Name	Category	Theorems
`objMk₁` 📖	CompOp	13 math math: `objMk₁_bijective`, `SSet.prodStdSimplex.nonDegenerateEquiv₁_snd`, `objMk₁_surjective`, `objMk₁_apply`, `σ_objMk₁_of_le`, `objMk₁_injective`, `objMk₁_of_castSucc_lt`, `objMk₁_of_le_castSucc`, `δ_objMk₁_of_le`, `objMk₁_apply_eq_zero_iff`, `σ_objMk₁_of_lt`, `δ_objMk₁_of_lt`, `objMk₁_apply_eq_one_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`objMk₁_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat` `objMk₁`	—	—
`objMk₁_apply_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat` `objMk₁`	—	`SimplexCategory.toMk₁_apply_eq_one_iff`
`objMk₁_apply_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat` `objMk₁`	—	`SimplexCategory.toMk₁_apply_eq_zero_iff`
`objMk₁_bijective` 📖	mathematical	—	`Function.Bijective` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `objMk₁`	—	`Equiv.bijective`
`objMk₁_injective` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `objMk₁`	—	`Function.Bijective.injective` `objMk₁_bijective`
`objMk₁_of_castSucc_lt` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat` `objMk₁`	—	`SimplexCategory.toMk₁_of_castSucc_lt`
`objMk₁_of_le_castSucc` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat` `objMk₁`	—	`SimplexCategory.toMk₁_of_le_castSucc`
`objMk₁_surjective` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `objMk₁`	—	`Function.Bijective.surjective` `objMk₁_bijective`
`δ_objMk₁_of_le` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `SSet.stdSimplex` `objMk₁` `Fin.castPred` `Fin.ne_last_of_lt` `lt_of_le_of_lt` `PartialOrder.toPreorder` `Fin.instPartialOrder`	—	`ext` `Fin.ne_last_of_lt` `lt_of_le_of_lt` `CategoryTheory.ConcreteCategory.congr_hom` `SimplexCategory.δ_comp_toMk₁_of_le`
`δ_objMk₁_of_lt` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `SSet.stdSimplex` `objMk₁` `Fin.ne_zero_of_lt`	—	`ext` `Fin.ne_zero_of_lt` `CategoryTheory.ConcreteCategory.congr_hom` `SimplexCategory.δ_comp_toMk₁_of_lt`
`σ_objMk₁_of_le` 📖	mathematical	—	`CategoryTheory.SimplicialObject.σ` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `SSet.stdSimplex` `objMk₁`	—	`ext` `CategoryTheory.ConcreteCategory.congr_hom` `SimplexCategory.σ_comp_toMk₁_of_le`
`σ_objMk₁_of_lt` 📖	mathematical	—	`CategoryTheory.SimplicialObject.σ` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `SSet.stdSimplex` `objMk₁`	—	`ext` `CategoryTheory.ConcreteCategory.congr_hom` `SimplexCategory.σ_comp_toMk₁_of_lt`

---

← Back to Index