Basic

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

Statistics

Metric	Count
Definitions `const`, `diag`, `factor_δ`, `instConcreteCategoryOrderHomFinHAddNatLenOfNat`, `instDecidableEqHom`, `instFintypeToTypeOrderHomFinHAddNatLenOfNat`, `instOfNatToTypeOrderHomFinHAddNatLenOfNat`, `intervalEdge`, `isTerminalZero`, `mkHom`, `mkOfLe`, `mkOfLeComp`, `mkOfSucc`, `orderIsoOfIso`, `skeletalEquivalence`, `skeletalFunctor`, `subinterval`, `toCat`, `topIsoZero`, `uniqueHomToZero`, `δ`, `σ`	22
Theorems `ext_one_left`, `ext_zero_left`, `instEssSurjNonemptyFinLinOrdSkeletalFunctor`, `instFaithfulNonemptyFinLinOrdSkeletalFunctor`, `instFullNonemptyFinLinOrdSkeletalFunctor`, `isEquivalence`, `concreteCategoryHom_id`, `congr_toOrderHom_apply`, `const_apply`, `const_comp`, `const_eq_id`, `const_fac_thru_zero`, `const_subinterval_eq`, `diag_subinterval_eq`, `epi_iff_surjective`, `eqToHom_toOrderHom`, `eq_comp_δ_of_not_surjective`, `eq_comp_δ_of_not_surjective'`, `eq_const_of_zero`, `eq_const_to_zero`, `eq_id_of_epi`, `eq_id_of_isIso`, `eq_id_of_mono`, `eq_of_isIso`, `eq_of_one_to_one`, `eq_of_one_to_two`, `eq_of_one_to_two'`, `eq_δ_of_mono`, `eq_σ_comp_of_not_injective`, `eq_σ_comp_of_not_injective'`, `eq_σ_of_epi`, `exists_eq_const_of_zero`, `factorThruImage_eq`, `factor_δ_spec`, `hom_zero_zero`, `image_eq`, `image_ι_eq`, `instBalanced`, `instEpiFactorThruImage`, `instEpiσ`, `instFiniteHom`, `instHasStrongEpiImages`, `instHasStrongEpiMonoFactorisations`, `instHasTerminal`, `instMonoδ`, `instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat`, `instSplitEpiCategory`, `instSubsingletonHomMkOfNatNat`, `isIso_iff_of_epi`, `isIso_iff_of_mono`, `isIso_of_bijective`, `isSkeletonOf`, `iso_eq_iso_refl`, `le_of_epi`, `le_of_mono`, `len_eq_of_isIso`, `len_le_of_epi`, `len_le_of_mono`, `len_lt_of_mono`, `mkOfLe_refl`, `mkOfSucc_eq_id`, `mkOfSucc_homToOrderHom_one`, `mkOfSucc_homToOrderHom_zero`, `mkOfSucc_one_eq_δ`, `mkOfSucc_subinterval_eq`, `mkOfSucc_zero_eq_δ`, `mkOfSucc_δ_eq`, `mkOfSucc_δ_gt`, `mkOfSucc_δ_lt`, `mono_iff_injective`, `skeletal`, `coe_map`, `skeletalFunctor_map`, `skeletalFunctor_obj`, `obj_eq_Fin`, `toCat_map`, `toCat_obj`, `toType_apply`, `δ_comp_δ`, `δ_comp_δ'`, `δ_comp_δ''`, `δ_comp_δ_self`, `δ_comp_δ_self'`, `δ_comp_δ_self'_assoc`, `δ_comp_δ_self_assoc`, `δ_comp_σ_of_gt`, `δ_comp_σ_of_gt'`, `δ_comp_σ_of_gt'_assoc`, `δ_comp_σ_of_gt_assoc`, `δ_comp_σ_of_le`, `δ_comp_σ_of_le_assoc`, `δ_comp_σ_self`, `δ_comp_σ_self'`, `δ_comp_σ_self'_assoc`, `δ_comp_σ_self_assoc`, `δ_comp_σ_succ`, `δ_comp_σ_succ'`, `δ_comp_σ_succ'_assoc`, `δ_comp_σ_succ_assoc`, `δ_injective`, `δ_one_eq_const`, `δ_one_mkOfSucc`, `δ_zero_eq_const`, `δ_zero_mkOfSucc`, `σ_comp_σ`, `σ_comp_σ_assoc`, `σ_injective`	107
Total	129

SimplexCategory

Definitions

Name	Category	Theorems
`const` 📖	CompOp	27 math math: `eq_const_of_zero`, `const_eq_id`, `eq_of_one_to_two`, `const_comp`, `const_subinterval_eq`, `CategoryTheory.CosimplicialObject.augment_hom_app`, `SSet.spine_vertex`, `δ_zero_mkOfSucc`, `const_fac_thru_zero`, `eq_const_to_zero`, `Truncated.δ₂_zero_eq_const`, `δ_one_eq_const`, `eq_of_one_to_two'`, `CategoryTheory.SimplicialObject.augment_hom_app`, `δ_zero_eq_const`, `SSet.const_app`, `SSet.Truncated.StrictSegal.spineToSimplex_vertex`, `Truncated.δ₂_one_eq_const`, `SSet.Truncated.spine_vertex`, `δ_one_mkOfSucc`, `mkOfLe_refl`, `const_apply`, `CategoryTheory.CosimplicialObject.equivalenceRightToLeft_right_app`, `eq_of_one_to_one`, `exists_eq_const_of_zero`, `CategoryTheory.SimplicialObject.equivalenceLeftToRight_left_app`, `SSet.StrictSegal.spineToSimplex_vertex`
`diag` 📖	CompOp	1 math math: `diag_subinterval_eq`
`factor_δ` 📖	CompOp	1 math math: `factor_δ_spec`
`instConcreteCategoryOrderHomFinHAddNatLenOfNat` 📖	CompOp	8 math math: `toTop_map`, `toTop₀_map`, `instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat`, `CategoryTheory.Limits.FormalCoproduct.cechFunctor_map_app`, `CategoryTheory.Limits.FormalCoproduct.cech_map`, `toType_apply`, `concreteCategoryHom_id`, `CategoryTheory.Limits.FormalCoproduct.cech_obj`
`instDecidableEqHom` 📖	CompOp	—
`instFintypeToTypeOrderHomFinHAddNatLenOfNat` 📖	CompOp	5 math math: `toTop_obj`, `toTop_map`, `toTop₀_map`, `toTop₀_obj`, `SSet.stdSimplex.face_obj`
`instOfNatToTypeOrderHomFinHAddNatLenOfNat` 📖	CompOp	8 math math: `CategoryTheory.CosimplicialObject.augment_hom_app`, `Truncated.δ₂_zero_eq_const`, `CategoryTheory.SimplicialObject.augment_hom_app`, `SSet.const_app`, `Truncated.δ₂_one_eq_const`, `CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0`, `CategoryTheory.SimplicialObject.equivalenceRightToLeft_left`, `CategoryTheory.CosimplicialObject.equivalenceLeftToRight_right`
`intervalEdge` 📖	CompOp	4 math math: `diag_subinterval_eq`, `SSet.StrictSegal.spineToSimplex_edge`, `SSet.Truncated.StrictSegal.spineToSimplex_edge`, `mkOfSucc_δ_eq`
`isTerminalZero` 📖	CompOp	—
`mkHom` 📖	CompOp	—
`mkOfLe` 📖	CompOp	2 math math: `SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂`, `mkOfLe_refl`
`mkOfLeComp` 📖	CompOp	—
`mkOfSucc` 📖	CompOp	18 math math: `mkOfSucc_eq_id`, `SSet.StrictSegalCore.map_mkOfSucc_zero_concat`, `mkOfSucc_homToOrderHom_one`, `δ_zero_mkOfSucc`, `mkOfSucc_subinterval_eq`, `SSet.spine_arrow`, `mkOfSucc_δ_lt`, `mkOfSucc_homToOrderHom_zero`, `SSet.Truncated.spine_arrow`, `SSet.Truncated.StrictSegal.spineToSimplex_arrow`, `δ_one_mkOfSucc`, `mkOfSucc_δ_gt`, `SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁`, `SSet.StrictSegalCore.map_mkOfSucc_zero_spineToSimplex`, `SSet.StrictSegal.spineToSimplex_arrow`, `mkOfSucc_zero_eq_δ`, `mkOfSucc_δ_eq`, `mkOfSucc_one_eq_δ`
`orderIsoOfIso` 📖	CompOp	—
`skeletalEquivalence` 📖	CompOp	—
`skeletalFunctor` 📖	CompOp	8 math math: `SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor`, `isSkeletonOf`, `SkeletalFunctor.isEquivalence`, `skeletalFunctor_obj`, `SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor`, `skeletalFunctor_map`, `skeletalFunctor.coe_map`, `SkeletalFunctor.instFullNonemptyFinLinOrdSkeletalFunctor`
`subinterval` 📖	CompOp	7 math math: `SSet.spine_map_subinterval`, `const_subinterval_eq`, `mkOfSucc_subinterval_eq`, `SSet.Truncated.spine_map_subinterval`, `SSet.StrictSegal.spineToSimplex_interval`, `diag_subinterval_eq`, `SSet.Truncated.StrictSegal.spineToSimplex_interval`
`toCat` 📖	CompOp	4 math math: `toCat.obj_eq_Fin`, `CategoryTheory.nerve_map`, `toCat_obj`, `toCat_map`
`topIsoZero` 📖	CompOp	—
`uniqueHomToZero` 📖	CompOp	—
`δ` 📖	CompOp	55 math math: `δ_comp_δ'`, `eq_of_one_to_two`, `δ_comp_δ''`, `δ_comp_σ_of_gt'_assoc`, `δ_comp_σ_self'`, `δ_comp_δ_self'`, `CategoryTheory.SimplicialObject.δ_def`, `II_σ`, `δ_comp_σ_self_assoc`, `δ_zero_mkOfSucc`, `δ_comp_σ_succ_assoc`, `δ_comp_δ_self`, `δ_comp_σ_of_gt'`, `δ_one_eq_const`, `eq_of_one_to_two'`, `mkOfSucc_δ_lt`, `AlgebraicTopology.DoldKan.Isδ₀.iff`, `SSet.Truncated.StrictSegal.spine_δ_arrow_lt`, `δ_comp_σ_of_le`, `factor_δ_spec`, `rev_map_δ`, `eq_comp_δ_of_not_surjective'`, `SSet.Truncated.StrictSegal.spine_δ_arrow_gt`, `AlgebraicTopology.DoldKan.Isδ₀.eq_δ₀`, `δ_zero_eq_const`, `δ_comp_δ_self'_assoc`, `δ_comp_σ_of_gt`, `SSet.Truncated.StrictSegal.spine_δ_vertex_ge`, `δ_comp_δ`, `δ_injective`, `δ_comp_δ_self_assoc`, `SSet.Truncated.Path.arrow_src`, `SimplexCategoryGenRel.toSimplexCategory_map_δ`, `δ_one_mkOfSucc`, `mkOfSucc_δ_gt`, `δ_comp_σ_of_gt_assoc`, `δ_comp_σ_succ'`, `SSet.Truncated.StrictSegal.spine_δ_arrow_eq`, `δ_comp_σ_self`, `SSet.Truncated.Path₁.arrow_tgt`, `δ_comp_σ_of_le_assoc`, `SSet.Truncated.Path.arrow_tgt`, `mkOfSucc_zero_eq_δ`, `mkOfSucc_δ_eq`, `δ_comp_σ_succ'_assoc`, `SSet.Truncated.Path₁.arrow_src`, `eq_δ_of_mono`, `SSet.Truncated.StrictSegal.spine_δ_vertex_lt`, `eq_comp_δ_of_not_surjective`, `mkOfSucc_one_eq_δ`, `δ_comp_σ_succ`, `SSet.stdSimplex.face_singleton_compl`, `AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀`, `instMonoδ`, `δ_comp_σ_self'_assoc`
`σ` 📖	CompOp	25 math math: `δ_comp_σ_of_gt'_assoc`, `δ_comp_σ_self'`, `σ_injective`, `δ_comp_σ_self_assoc`, `δ_comp_σ_succ_assoc`, `δ_comp_σ_of_gt'`, `eq_σ_comp_of_not_injective`, `SimplexCategoryGenRel.toSimplexCategory_map_σ`, `CategoryTheory.SimplicialObject.σ_def`, `δ_comp_σ_of_le`, `σ_comp_σ_assoc`, `rev_map_σ`, `δ_comp_σ_of_gt`, `eq_σ_of_epi`, `instEpiσ`, `eq_σ_comp_of_not_injective'`, `δ_comp_σ_of_gt_assoc`, `δ_comp_σ_succ'`, `δ_comp_σ_self`, `δ_comp_σ_of_le_assoc`, `δ_comp_σ_succ'_assoc`, `σ_comp_σ`, `II_δ`, `δ_comp_σ_succ`, `δ_comp_σ_self'_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`concreteCategoryHom_id` 📖	mathematical	—	`CategoryTheory.ConcreteCategory.hom` `SimplexCategory` `smallCategory` `OrderHom` `len` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `instConcreteCategoryOrderHomFinHAddNatLenOfNat` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `OrderHom.id`	—	—
`congr_toOrderHom_apply` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `len` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom`	—	—
`const_apply` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `len` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom` `const`	—	—
`const_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `const` `DFunLike.coe` `OrderHom` `len` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom`	—	—
`const_eq_id` 📖	mathematical	—	`const` `len` `CategoryTheory.CategoryStruct.id` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory`	—	`Hom.ext` `OrderHom.ext`
`const_fac_thru_zero` 📖	mathematical	—	`const` `CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `len`	—	`const_comp`
`const_subinterval_eq` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `const` `subinterval` `len` `lt_add_of_lt_add_right` `Nat.instPreorder` `covariant_swap_add_of_covariant_add` `Preorder.toLE` `Nat.instAddCommSemigroup` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instIsOrderedAddMonoid`	—	`lt_add_of_lt_add_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `const_comp` `add_comm`
`diag_subinterval_eq` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `diag` `subinterval` `intervalEdge`	—	`Hom.ext` `OrderHom.ext` `zero_add`
`epi_iff_surjective` 📖	mathematical	—	`CategoryTheory.Epi` `SimplexCategory` `smallCategory` `len` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom`	—	`CategoryTheory.Functor.epi_map_iff_epi` `CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape` `CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsColimits` `CategoryTheory.Limits.fullyFaithful_reflectsColimits` `CategoryTheory.Equivalence.full_functor` `CategoryTheory.Equivalence.faithful_functor` `CategoryTheory.ConcreteCategory.hom_ofHom`
`eqToHom_toOrderHom` 📖	mathematical	—	`Hom.toOrderHom` `CategoryTheory.eqToHom` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `OrderEmbedding.toOrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderIso.toOrderEmbedding` `Fin.castOrderIso` `len`	—	—
`eq_comp_δ_of_not_surjective` 📖	mathematical	`len` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom`	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ`	—	`eq_comp_δ_of_not_surjective'`
`eq_comp_δ_of_not_surjective'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ`	—	`Hom.ext` `OrderHom.ext` `Fin.predAbove_right_last` `Fin.predAbove_last_of_ne_last` `Fin.succAbove_last` `Fin.castSucc_castPred` `Fin.succAbove_predAbove`
`eq_const_of_zero` 📖	mathematical	—	`const` `DFunLike.coe` `OrderHom` `len` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom`	—	`Hom.ext` `OrderHom.ext`
`eq_const_to_zero` 📖	mathematical	—	`const` `len`	—	`Hom.ext` `OrderHom.ext`
`eq_id_of_epi` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory`	—	`isIso_of_bijective` `Fintype.bijective_iff_surjective_and_card` `epi_iff_surjective` `eq_id_of_isIso`
`eq_id_of_isIso` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory`	—	`iso_eq_iso_refl`
`eq_id_of_mono` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory`	—	`isIso_of_bijective` `Fintype.bijective_iff_injective_and_card` `mono_iff_injective` `eq_id_of_isIso`
`eq_of_isIso` 📖	—	—	—	—	`len_eq_of_isIso`
`eq_of_one_to_one` 📖	mathematical	—	`const` `CategoryTheory.CategoryStruct.id` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory`	—	`Hom.ext` `OrderHom.ext` `OrderHom.monotone`
`eq_of_one_to_two` 📖	mathematical	—	`δ` `const`	—	`OrderHom.monotone` `Hom.ext` `OrderHom.ext`
`eq_of_one_to_two'` 📖	mathematical	—	`δ` `const`	—	`eq_of_one_to_two`
`eq_δ_of_mono` 📖	mathematical	—	`δ`	—	`eq_comp_δ_of_not_surjective` `epi_iff_surjective` `eq_id_of_mono` `CategoryTheory.mono_of_mono` `CategoryTheory.Category.id_comp`
`eq_σ_comp_of_not_injective` 📖	mathematical	`len` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom`	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `σ`	—	`LT.lt.ne` `LE.le.trans_lt'` `eq_σ_comp_of_not_injective'` `le_antisymm` `OrderHom.monotone` `le_of_lt` `Fin.castSucc_castPred` `Fin.succ_castPred_le_iff`
`eq_σ_comp_of_not_injective'` 📖	mathematical	`DFunLike.coe` `OrderHom` `len` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom`	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `σ`	—	`Hom.ext` `OrderHom.ext` `Fin.predAbove_of_le_castSucc` `Fin.succAbove_of_castSucc_lt` `Fin.castSucc_lt_succ_iff` `Fin.castSucc_castPred` `Fin.ne_zero_of_lt` `Fin.predAbove_of_castSucc_lt` `Fin.succAbove_of_le_castSucc`
`eq_σ_of_epi` 📖	mathematical	—	`σ`	—	`eq_σ_comp_of_not_injective` `mono_iff_injective` `eq_id_of_epi` `CategoryTheory.epi_of_epi` `CategoryTheory.Category.comp_id`
`exists_eq_const_of_zero` 📖	mathematical	—	`const`	—	`eq_const_of_zero`
`factorThruImage_eq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `CategoryTheory.Limits.image` `CategoryTheory.Limits.HasImages.has_image` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `instHasStrongEpiMonoFactorisations`	`CategoryTheory.Limits.factorThruImage`	—	`CategoryTheory.Limits.HasImages.has_image` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `instHasStrongEpiMonoFactorisations` `CategoryTheory.cancel_mono` `image_ι_eq` `CategoryTheory.Limits.image.fac`
`factor_δ_spec` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `factor_δ` `δ`	—	`Hom.ext` `OrderHom.ext` `Fin.predAbove_right_zero` `CategoryTheory.Category.assoc` `Fin.predAbove_zero_of_ne_zero` `Fin.succ_succAbove_predAbove`
`hom_zero_zero` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory`	—	`instSubsingletonHomMkOfNatNat`
`image_eq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory`	`CategoryTheory.Limits.image` `CategoryTheory.Limits.HasImages.has_image` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `instHasStrongEpiMonoFactorisations`	—	`CategoryTheory.Limits.HasImages.has_image` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `instHasStrongEpiMonoFactorisations` `CategoryTheory.strongEpi_of_epi` `CategoryTheory.strongEpiCategory_of_regularEpiCategory` `CategoryTheory.regularEpiCategoryOfSplitEpiCategory` `instSplitEpiCategory` `ext` `le_antisymm` `len_le_of_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_hom` `len_le_of_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso`
`image_ι_eq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `CategoryTheory.Limits.image` `CategoryTheory.Limits.HasImages.has_image` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `instHasStrongEpiMonoFactorisations`	`CategoryTheory.Limits.image.ι`	—	`CategoryTheory.Limits.HasImages.has_image` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `instHasStrongEpiMonoFactorisations` `CategoryTheory.strongEpi_of_epi` `CategoryTheory.strongEpiCategory_of_regularEpiCategory` `CategoryTheory.regularEpiCategoryOfSplitEpiCategory` `instSplitEpiCategory` `CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι` `eq_id_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Category.id_comp`
`instBalanced` 📖	mathematical	—	`CategoryTheory.Balanced` `SimplexCategory` `smallCategory`	—	`isIso_iff_of_epi` `le_antisymm` `len_le_of_mono` `len_le_of_epi`
`instEpiFactorThruImage` 📖	mathematical	—	`CategoryTheory.Epi` `SimplexCategory` `smallCategory` `CategoryTheory.Limits.image` `CategoryTheory.Limits.HasImages.has_image` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.factorThruImage`	—	`CategoryTheory.StrongEpi.epi` `CategoryTheory.Limits.HasImages.has_image` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `instHasStrongEpiMonoFactorisations` `CategoryTheory.Limits.HasStrongEpiImages.strong_factorThruImage` `instHasStrongEpiImages`
`instEpiσ` 📖	mathematical	—	`CategoryTheory.Epi` `SimplexCategory` `smallCategory` `σ`	—	`Fin.predAbove_surjective`
`instFiniteHom` 📖	mathematical	—	`Finite` `Quiver.Hom` `SimplexCategory` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `smallCategory`	—	`Finite.of_injective` `Pi.finite` `Finite.of_fintype`
`instHasStrongEpiImages` 📖	mathematical	—	`CategoryTheory.Limits.HasStrongEpiImages` `SimplexCategory` `smallCategory` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `instHasStrongEpiMonoFactorisations`	—	`CategoryTheory.Limits.hasStrongEpiImages_of_hasStrongEpiMonoFactorisations` `instHasStrongEpiMonoFactorisations`
`instHasStrongEpiMonoFactorisations` 📖	mathematical	—	`CategoryTheory.Limits.HasStrongEpiMonoFactorisations` `SimplexCategory` `smallCategory`	—	`CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_inverse` `NonemptyFinLinOrd.instHasStrongEpiMonoFactorisations`
`instHasTerminal` 📖	mathematical	—	`CategoryTheory.Limits.HasTerminal` `SimplexCategory` `smallCategory`	—	`CategoryTheory.Limits.IsTerminal.hasTerminal`
`instMonoδ` 📖	mathematical	—	`CategoryTheory.Mono` `SimplexCategory` `smallCategory` `δ`	—	`mono_iff_injective` `Fin.succAbove_right_injective`
`instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `SimplexCategory` `smallCategory` `CategoryTheory.types` `CategoryTheory.forget` `OrderHom` `len` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `instConcreteCategoryOrderHomFinHAddNatLenOfNat`	—	`CategoryTheory.Iso.isIso_hom` `not_le` `CategoryTheory.ConcreteCategory.congr_hom` `CategoryTheory.Iso.inv_hom_id` `OrderHom.monotone` `le_of_not_ge` `eq_of_le_of_not_lt` `le_refl` `Hom.ext` `OrderHom.ext` `CategoryTheory.Iso.hom_inv_id`
`instSplitEpiCategory` 📖	mathematical	—	`CategoryTheory.SplitEpiCategory` `SimplexCategory` `smallCategory`	—	`CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence` `CategoryTheory.Equivalence.isEquivalence_inverse` `NonemptyFinLinOrd.instSplitEpiCategory`
`instSubsingletonHomMkOfNatNat` 📖	mathematical	—	`Quiver.Hom` `SimplexCategory` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `smallCategory`	—	`Hom.ext` `OrderHom.ext`
`isIso_iff_of_epi` 📖	mathematical	—	`CategoryTheory.IsIso` `SimplexCategory` `smallCategory` `len`	—	`len_eq_of_isIso` `isIso_of_bijective` `Finite.injective_iff_surjective` `Finite.of_fintype` `epi_iff_surjective`
`isIso_iff_of_mono` 📖	mathematical	—	`CategoryTheory.IsIso` `SimplexCategory` `smallCategory` `len`	—	`len_eq_of_isIso` `isIso_of_bijective` `mono_iff_injective` `Finite.injective_iff_surjective` `Finite.of_fintype`
`isIso_of_bijective` 📖	mathematical	`Function.Bijective` `len` `OrderHom.toFun` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Hom.toOrderHom`	`CategoryTheory.IsIso` `SimplexCategory` `smallCategory`	—	`CategoryTheory.isIso_of_reflects_iso` `CategoryTheory.isIso_iff_bijective` `instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat`
`isSkeletonOf` 📖	mathematical	—	`CategoryTheory.IsSkeletonOf` `NonemptyFinLinOrd` `NonemptyFinLinOrd.instLargeCategory` `SimplexCategory` `smallCategory` `skeletalFunctor`	—	`skeletal` `SkeletalFunctor.isEquivalence`
`iso_eq_iso_refl` 📖	mathematical	—	`CategoryTheory.Iso.refl` `SimplexCategory` `smallCategory`	—	`Finset.card_fin` `Finset.orderEmbOfFin_unique'` `Finset.mem_univ` `CategoryTheory.Iso.ext` `Hom.ext` `OrderHom.ext`
`le_of_epi` 📖	—	—	—	—	`len_le_of_epi`
`le_of_mono` 📖	—	—	—	—	`len_le_of_mono`
`len_eq_of_isIso` 📖	mathematical	—	`len`	—	`le_antisymm` `len_le_of_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `len_le_of_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso`
`len_le_of_epi` 📖	mathematical	—	`len`	—	`Fintype.card_fin` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Fintype.card_le_of_surjective` `epi_iff_surjective`
`len_le_of_mono` 📖	mathematical	—	`len`	—	`Fintype.card_fin` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Fintype.card_le_of_injective` `mono_iff_injective`
`len_lt_of_mono` 📖	mathematical	—	`len`	—	—
`mkOfLe_refl` 📖	mathematical	—	`mkOfLe` `const`	—	`Hom.ext_one_left`
`mkOfSucc_eq_id` 📖	mathematical	—	`mkOfSucc` `CategoryTheory.CategoryStruct.id` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory`	—	—
`mkOfSucc_homToOrderHom_one` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom` `mkOfSucc`	—	—
`mkOfSucc_homToOrderHom_zero` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom` `mkOfSucc`	—	—
`mkOfSucc_one_eq_δ` 📖	mathematical	—	`mkOfSucc` `δ`	—	—
`mkOfSucc_subinterval_eq` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `mkOfSucc` `subinterval`	—	`Hom.ext` `OrderHom.ext`
`mkOfSucc_zero_eq_δ` 📖	mathematical	—	`mkOfSucc` `δ`	—	—
`mkOfSucc_δ_eq` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `mkOfSucc` `δ` `intervalEdge`	—	`Hom.ext` `OrderHom.ext` `Fintype.complete` `Fin.castSucc_succAbove_castSucc` `Fin.succAbove_succ_self` `Fin.succAbove_castSucc_self`
`mkOfSucc_δ_gt` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `mkOfSucc` `δ`	—	`Hom.ext` `OrderHom.ext` `Fintype.complete` `Fin.succAbove_of_le_castSucc`
`mkOfSucc_δ_lt` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `mkOfSucc` `δ`	—	`Hom.ext` `OrderHom.ext` `Fintype.complete` `Fin.succAbove_of_castSucc_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass`
`mono_iff_injective` 📖	mathematical	—	`CategoryTheory.Mono` `SimplexCategory` `smallCategory` `len` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `Hom.toOrderHom`	—	`CategoryTheory.Functor.mono_map_iff_mono` `CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape` `CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits` `CategoryTheory.Limits.fullyFaithful_reflectsLimits` `CategoryTheory.Equivalence.full_functor` `CategoryTheory.Equivalence.faithful_functor` `CategoryTheory.ConcreteCategory.hom_ofHom`
`skeletal` 📖	mathematical	—	`CategoryTheory.Skeletal` `SimplexCategory` `smallCategory`	—	`Fintype.card_congr` `ext` `Fintype.card_fin`
`skeletalFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `SimplexCategory` `smallCategory` `NonemptyFinLinOrd` `NonemptyFinLinOrd.instLargeCategory` `skeletalFunctor` `NonemptyFinLinOrd.ofHom` `len` `Fin.instLinearOrder` `Fin.fintype` `Hom.toOrderHom`	—	—
`skeletalFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `SimplexCategory` `smallCategory` `NonemptyFinLinOrd` `NonemptyFinLinOrd.instLargeCategory` `skeletalFunctor` `NonemptyFinLinOrd.of` `len` `Fin.fintype` `Fin.instLinearOrder`	—	—
`toCat_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `SimplexCategory` `smallCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `toCat` `CategoryTheory.Functor.toCatHom` `Preord.carrier` `CategoryTheory.Functor.obj` `PartOrd` `PartOrd.instCategory` `Preord` `Preord.instCategory` `CategoryTheory.forget₂` `OrderHom` `PartOrd.carrier` `PartialOrder.toPreorder` `PartOrd.str` `OrderHom.instFunLike` `PartOrd.instConcreteCategoryOrderHomCarrier` `Preord.str` `Preord.instConcreteCategoryOrderHomCarrier` `PartOrd.hasForgetToPreord` `Lat` `Lat.instCategory` `LatticeHom` `Lat.carrier` `Lat.str` `LatticeHom.instFunLike` `Lat.instConcreteCategoryLatticeHomCarrier` `Lat.hasForgetToPartOrd` `LinOrd` `LinOrd.instCategory` `LinOrd.carrier` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinOrd.str` `LinOrd.instConcreteCategoryOrderHomCarrier` `LinOrd.hasForgetToLat` `NonemptyFinLinOrd` `NonemptyFinLinOrd.instLargeCategory` `NonemptyFinLinOrd.toLinOrd` `NonemptyFinLinOrd.instConcreteCategoryOrderHomCarrier` `NonemptyFinLinOrd.hasForgetToLinOrd` `NonemptyFinLinOrd.of` `len` `Fin.fintype` `Fin.instLinearOrder` `Preorder.smallCategory` `Monotone.functor` `DFunLike.coe` `Preord.Hom.hom` `NonemptyFinLinOrd.ofHom` `Hom.toOrderHom`	—	—
`toCat_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `SimplexCategory` `smallCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `toCat` `CategoryTheory.Cat.of` `Preord.carrier` `PartOrd` `PartOrd.instCategory` `Preord` `Preord.instCategory` `CategoryTheory.forget₂` `OrderHom` `PartOrd.carrier` `PartialOrder.toPreorder` `PartOrd.str` `OrderHom.instFunLike` `PartOrd.instConcreteCategoryOrderHomCarrier` `Preord.str` `Preord.instConcreteCategoryOrderHomCarrier` `PartOrd.hasForgetToPreord` `Lat` `Lat.instCategory` `LatticeHom` `Lat.carrier` `Lat.str` `LatticeHom.instFunLike` `Lat.instConcreteCategoryLatticeHomCarrier` `Lat.hasForgetToPartOrd` `LinOrd` `LinOrd.instCategory` `LinOrd.carrier` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinOrd.str` `LinOrd.instConcreteCategoryOrderHomCarrier` `LinOrd.hasForgetToLat` `NonemptyFinLinOrd` `NonemptyFinLinOrd.instLargeCategory` `NonemptyFinLinOrd.toLinOrd` `NonemptyFinLinOrd.instConcreteCategoryOrderHomCarrier` `NonemptyFinLinOrd.hasForgetToLinOrd` `NonemptyFinLinOrd.of` `len` `Fin.fintype` `Fin.instLinearOrder` `Preorder.smallCategory`	—	—
`toType_apply` 📖	mathematical	—	`CategoryTheory.ToType` `SimplexCategory` `smallCategory` `OrderHom` `len` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `instConcreteCategoryOrderHomFinHAddNatLenOfNat`	—	—
`δ_comp_δ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ`	—	`Hom.ext` `OrderHom.ext` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le`
`δ_comp_δ'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ`	—	`δ_comp_δ`
`δ_comp_δ''` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `Fin.le_iff_val_le_val`	—	`Fin.le_iff_val_le_val` `δ_comp_δ`
`δ_comp_δ_self` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ`	—	`δ_comp_δ` `le_refl`
`δ_comp_δ_self'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ`	—	`δ_comp_δ_self`
`δ_comp_δ_self'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_comp_δ_self'`
`δ_comp_δ_self_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_comp_δ_self`
`δ_comp_σ_of_gt` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ`	—	`Hom.ext` `OrderHom.ext` `le_or_gt` `Fin.succAbove_of_castSucc_lt` `Fin.castSucc_lt_succ_iff` `Fin.castSucc_le_castSucc_iff` `Fin.predAbove_of_le_castSucc` `Iff.not` `LT.lt.ne` `Fin.castPred_castSucc` `Fin.castSucc_castPred` `LE.le.trans_lt` `Fin.ne_zero_of_lt` `Fin.predAbove_of_castSucc_lt` `Fin.castSucc_pred_eq_pred_castSucc` `Fin.succAbove_of_le_castSucc` `Fin.succ_le_castSucc_iff` `LT.lt.trans` `LT.lt.le` `Fin.le_castSucc_pred_iff`
`δ_comp_σ_of_gt'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ` `add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instPartialOrder` `covariant_swap_add_of_covariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Nat.instAddCommSemigroup` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instAddCommMonoid` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Nat.instLinearOrder` `lt_of_lt_of_le` `Nat.instPreorder`	—	`add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `lt_of_lt_of_le` `δ_comp_σ_of_gt`
`δ_comp_σ_of_gt'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ` `add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instPartialOrder` `covariant_swap_add_of_covariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Nat.instAddCommSemigroup` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instAddCommMonoid` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Nat.instLinearOrder` `lt_of_lt_of_le` `Nat.instPreorder`	—	`add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `lt_of_lt_of_le` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_comp_σ_of_gt'`
`δ_comp_σ_of_gt_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_comp_σ_of_gt`
`δ_comp_σ_of_le` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ`	—	`Hom.ext` `OrderHom.ext` `le_or_gt` `Fin.succAbove_of_le_castSucc` `Fin.castSucc_le_castSucc_iff` `Fin.succ_predAbove_succ` `Fin.predAbove_of_le_castSucc` `Fin.castSucc_castPred` `Fin.ne_zero_of_lt` `Fin.predAbove_of_castSucc_lt` `LE.le.trans_lt` `Fin.succAbove_of_castSucc_lt` `LE.le.trans_lt'` `LT.lt.le` `LT.lt.trans` `Iff.not` `LT.lt.ne` `Fin.castPred_castSucc`
`δ_comp_σ_of_le_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_comp_σ_of_le`
`δ_comp_σ_self` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ` `CategoryTheory.CategoryStruct.id`	—	`Hom.ext` `OrderHom.ext` `Fin.castPred.congr_simp` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`δ_comp_σ_self'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ` `CategoryTheory.CategoryStruct.id`	—	`δ_comp_σ_self`
`δ_comp_σ_self'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_comp_σ_self'`
`δ_comp_σ_self_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_comp_σ_self`
`δ_comp_σ_succ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ` `CategoryTheory.CategoryStruct.id`	—	`Hom.ext` `OrderHom.ext` `Fin.castPred.congr_simp`
`δ_comp_σ_succ'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ` `CategoryTheory.CategoryStruct.id`	—	`δ_comp_σ_succ`
`δ_comp_σ_succ'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_comp_σ_succ'`
`δ_comp_σ_succ_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `σ`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_comp_σ_succ`
`δ_injective` 📖	mathematical	—	`Quiver.Hom` `SimplexCategory` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ`	—	—
`δ_one_eq_const` 📖	mathematical	—	`δ` `const` `len`	—	—
`δ_one_mkOfSucc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `mkOfSucc` `const`	—	`Hom.ext` `OrderHom.ext` `Fintype.complete`
`δ_zero_eq_const` 📖	mathematical	—	`δ` `const` `len`	—	—
`δ_zero_mkOfSucc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `δ` `mkOfSucc` `const`	—	`Hom.ext` `OrderHom.ext` `Fintype.complete`
`σ_comp_σ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `σ`	—	`Hom.ext` `OrderHom.ext` `Fin.predAbove_right_last` `Fin.predAbove_right_zero` `le_or_gt` `Fin.ne_zero_of_lt` `Fin.castSucc_lt_succ_iff` `Fin.predAbove_of_castSucc_lt` `Fin.succ_predAbove_succ` `Fin.castSucc_le_castSucc_iff` `Fin.predAbove_of_le_castSucc` `Iff.not` `LT.lt.ne` `Fin.castPred_castSucc` `Fin.le_pred_iff` `Fin.succ_le_castSucc_iff` `LE.le.trans_lt` `LE.le.trans` `LT.lt.le` `LE.le.trans_lt'`
`σ_comp_σ_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategory` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `σ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `σ_comp_σ`
`σ_injective` 📖	mathematical	—	`Quiver.Hom` `SimplexCategory` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `smallCategory` `σ`	—	—

SimplexCategory.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_one_left` 📖	—	`SimplexCategory.len` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `toOrderHom`	—	—	`ext` `OrderHom.ext`
`ext_zero_left` 📖	—	`SimplexCategory.len` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `toOrderHom`	—	—	`ext` `OrderHom.ext`

SimplexCategory.SkeletalFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEssSurjNonemptyFinLinOrdSkeletalFunctor` 📖	mathematical	—	`CategoryTheory.Functor.EssSurj` `SimplexCategory` `NonemptyFinLinOrd` `SimplexCategory.smallCategory` `NonemptyFinLinOrd.instLargeCategory` `SimplexCategory.skeletalFunctor`	—	`Fintype.card_pos_iff` `OrderEmbedding.strictMono` `StrictMono.monotone` `StrictMono.le_iff_le` `OrderIso.apply_symm_apply` `NonemptyFinLinOrd.hom_ext` `OrderHom.ext` `OrderIso.symm_apply_apply`
`instFaithfulNonemptyFinLinOrdSkeletalFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `SimplexCategory` `SimplexCategory.smallCategory` `NonemptyFinLinOrd` `NonemptyFinLinOrd.instLargeCategory` `SimplexCategory.skeletalFunctor`	—	`SimplexCategory.Hom.ext` `OrderHom.ext` `CategoryTheory.congr_fun`
`instFullNonemptyFinLinOrdSkeletalFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Full` `SimplexCategory` `SimplexCategory.smallCategory` `NonemptyFinLinOrd` `NonemptyFinLinOrd.instLargeCategory` `SimplexCategory.skeletalFunctor`	—	—
`isEquivalence` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `SimplexCategory` `SimplexCategory.smallCategory` `NonemptyFinLinOrd` `NonemptyFinLinOrd.instLargeCategory` `SimplexCategory.skeletalFunctor`	—	`instFaithfulNonemptyFinLinOrdSkeletalFunctor` `instFullNonemptyFinLinOrdSkeletalFunctor` `instEssSurjNonemptyFinLinOrdSkeletalFunctor`

SimplexCategory.skeletalFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_map` 📖	mathematical	—	`LinOrd.Hom.hom` `NonemptyFinLinOrd.toLinOrd` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `NonemptyFinLinOrd` `NonemptyFinLinOrd.instLargeCategory` `SimplexCategory.skeletalFunctor` `CategoryTheory.InducedCategory.Hom.hom` `LinOrd` `LinOrd.instCategory` `CategoryTheory.Functor.map` `SimplexCategory.Hom.toOrderHom`	—	—

SimplexCategory.toCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`obj_eq_Fin` 📖	mathematical	—	`CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `SimplexCategory.toCat`	—	—

---

← Back to Index