StdSimplex

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

Statistics

Metric	Count
Definitions stdSimplex, S1, instInhabited, instInhabitedTruncated, stdSimplex, asOrderHom, const, edge, face, facePairIso, faceRepresentableBy, faceSingletonComplIso, faceSingletonIso, finSuccAboveOrderIsoFinset, instDecidableEqHomObjSimplexCategoryOfOppositeOp, instDecidableEqObjOppositeSimplexCategory, instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat, isoNerve, isoOfRepresentableBy, nonDegenerateEquiv, objEquiv, objMk, obj₀Equiv, triangle, yonedaEquiv, «termΔ[_]»	26
Theorems stdSimplex_map_left, stdSimplex_map_right, stdSimplex_obj_hom_app, stdSimplex_obj_left, stdSimplex_obj_right, range_eq_ofSimplex, yonedaEquiv_coe, coe_edge_down_toOrderHom, coe_triangle_down_toOrderHom, const_down_toOrderHom, ext, ext_iff, faceSingletonComplIso_hom_ι, faceSingletonComplIso_hom_ι_assoc, faceSingletonIso_one_hom_comp_ι_eq_δ, faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, faceSingletonIso_zero_hom_comp_ι_eq_δ, faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, face_eq_ofSimplex, face_inter_face, face_le_face_iff, face_obj, face_singleton_compl, instFiniteObjOppositeSimplexCategory, instFiniteObjSimplexCategory, instFiniteToSSetOfSimplex, instHasDimensionLEObjSimplexCategoryMk, isoNerve_hom_app_apply, isoNerve_inv_app_apply, map_apply, map_id, mem_face_iff, mem_nonDegenerate_iff_mono, mem_nonDegenerate_iff_strictMono, monotone_apply, nonDegenerateEquiv_apply_apply, nonDegenerateEquiv_symm_apply_coe, objEquiv_symm_apply, objEquiv_symm_comp, objEquiv_symm_mem_nonDegenerate_iff_mono, objEquiv_toOrderHom_apply, objMk_apply, objMk_bijective, obj₀Equiv_apply, obj₀Equiv_symm_apply, obj₀Equiv_symm_mem_face_iff, ofSimplex_yonedaEquiv_δ, range_δ, yonedaEquiv_map, yonedaEquiv_symm_app_objEquiv_symm, δ_objEquiv_symm_apply, δ_one_eq_const, δ_zero_eq_const, σ_objEquiv_symm_apply, yonedaEquiv_comp, yonedaEquiv_const, yonedaEquiv_symm_comp, yonedaEquiv_symm_zero	58
Total	84

SSet

Definitions

Name	Category	Theorems
S1 📖	CompOp	—
instInhabited 📖	CompOp	—
instInhabitedTruncated 📖	CompOp	—
stdSimplex 📖	CompOp	206 math math: stdSimplex.objMk_bijective, stdSimplex.mem_nonDegenerate_iff_strictMono, PtSimplex.RelStruct.δ_map_of_lt, horn₃₁.desc.multicofork_π_two, stdSimplex.δ_zero_eq_const, ι₀_snd_assoc, instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, horn.faceSingletonComplIso_inv_ι_assoc, stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ, stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ, stdSimplex.obj₀Equiv_symm_apply, horn₃₁.exists_desc, Subcomplex.range_eq_ofSimplex, PtSimplex.MulStruct.δ_map_of_gt, SimplexCategory.toTopHomeo_symm_naturality, prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, stdSimplex.objMk₁_bijective, horn.yonedaEquiv_ι, Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex, instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex, horn₃₂.desc.multicofork_π_one, yonedaEquiv_symm_zero, prodStdSimplex.orderHomOfSimplex_coe, horn₃₂.ι₁_desc, prodStdSimplex.nonDegenerateEquiv₁_snd, SimplexCategory.toTopHomeo_naturality_apply, RelativeMorphism.Homotopy.h₀_assoc, prodStdSimplex.objEquiv_apply_fst, stdSimplex.map_id, Homotopy.h₁_assoc, stdSimplex.objMk₁_surjective, horn₂₂.sq, stdSimplex.ext_iff, prodStdSimplex.strictMono_orderHomOfSimplex_iff, sSetTopAdj_homEquiv_stdSimplex_zero, horn₃₁.ι₂_desc_assoc, Subcomplex.ofSimplexProd_eq_range, stdSimplex.face_eq_ofSimplex, PtSimplex.RelStruct.δ_castSucc_map, stdSimplex.obj₀Equiv_apply, horn₃₁.desc.multicofork_pt, prodStdSimplex.objEquiv_δ_apply, horn.faceSingletonComplIso_inv_ι, stdSimplex.δ_zero_toSSetObjI, horn₃₁.ι₃_desc_assoc, prodStdSimplex.objEquiv_naturality, modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration, stdSimplex.spineId_arrow_apply_zero, yonedaEquiv_symm_comp, stdSimplex.range_δ, PtSimplex.RelStruct.δ_castSucc_map_assoc, PtSimplex.MulStruct.δ_succ_succ_map_assoc, stdSimplex.objMk₁_apply, stdSimplex.δ_objEquiv_symm_apply, stdSimplex.toSSetObj_app_const_zero, stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc, Augmented.stdSimplex_map_right, PtSimplex.MulStruct.δ_succ_succ_map, prodStdSimplex.objEquiv_apply_snd, Augmented.stdSimplex_obj_left, stdSimplex.σ_objMk₁_of_le, stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, horn₃₁.desc.multicofork_π_two_assoc, ι₁_app_snd_apply, stdSimplex.objMk₁_injective, horn.spineId_map_hornInclusion, horn₃₁.desc.multicofork_π_zero_assoc, horn_obj, ι₀_fst_assoc, ι₁_comp, Subcomplex.yonedaEquiv_coe, stdSimplex.face_obj, stdSimplex.nonDegenerateEquiv_apply_apply, modelCategoryQuillen.horn_ι_mem_J, stdSimplex.map_apply, ι₀_snd, PtSimplex.MulStruct.δ_succ_castSucc_map, Homotopy.h₀, stdSimplex.yonedaEquiv_symm_app_objEquiv_symm, horn₂₀.sq, horn₃₂.exists_desc, stdSimplex.mem_face_iff, SimplexCategory.toTopHomeo_symm_naturality_apply, stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ, ι₁_snd_assoc, horn.edge_coe, horn₃₁.ι₂_desc, stdSimplex.isoNerve_hom_app_apply, stdSimplex.faceSingletonComplIso_hom_ι, ι₁_app_fst, ι₁_snd, stdSimplex.objMk₁_of_castSucc_lt, stdSimplex.σ_objEquiv_symm_apply, horn₃₂.ι₃_desc, stdSimplex.instFiniteObjOppositeSimplexCategory, horn₃₂.ι₀_desc, face_le_horn, stdSimplex.objMk₁_of_le_castSucc, SimplexCategory.toTopHomeo_naturality, PtSimplex.MulStruct.δ_map_of_lt, stdSimplex.instHasDimensionLEObjSimplexCategoryMk, stdSimplex.monotone_apply, horn.faceι_ι, stdSimplex.δ_one_toSSetObjI, prodStdSimplex.objEquiv_map_apply, stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex, horn.edge₃_coe_down, horn₂₁.isPushout, horn_eq_iSup, yonedaEquiv_const, stdSimplex.obj₀Equiv_symm_mem_face_iff, prodStdSimplex.nonDegenerateEquiv₁_fst, prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, stdSimplex.objEquiv_symm_comp, ι₀_comp_assoc, horn₃₂.ι₁_desc_assoc, ι₀_comp, horn₃₂.desc.multicofork_π_zero_assoc, Homotopy.h₀_assoc, Augmented.stdSimplex_obj_hom_app, horn.faceι_ι_assoc, Homotopy.h₁, stdSimplex.δ_objMk₁_of_le, prodStdSimplex.le_orderHomOfSimplex, RelativeMorphism.Homotopy.h₁_assoc, stdSimplex.yonedaEquiv_map, RelativeMorphism.Homotopy.ofEq_h, horn_obj_zero, horn.spineId_vertex_coe, horn.multicoequalizerDiagram, horn.spineId_arrow_coe, stdSimplex.objEquiv_toOrderHom_apply, ι₁_fst, horn₃₁.desc.multicofork_π_three_assoc, PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, ι₀_app_snd_apply, horn₃₁.desc.multicofork_π_zero, horn₂₀.isPushout, stdSimplex.ofSimplex_yonedaEquiv_δ, prodStdSimplex.nonDegenerate_iff_injective_objEquiv, Quasicategory.hornFilling, prodStdSimplex.nonDegenerate_max_dim_iff, stdSimplex.instFiniteObjSimplexCategory, stdSimplex.objMk_apply, horn₃₂.desc.multicofork_π_three, RelativeMorphism.Homotopy.h₀, horn₃₁.ι₀_desc_assoc, modelCategoryQuillen.boundary_ι_mem_I, Augmented.stdSimplex_map_left, stdSimplex.faceSingletonComplIso_hom_ι_assoc, RelativeMorphism.Homotopy.precomp_h, ι₀_fst, stdSimplex.δ_one_eq_const, boundary_eq_iSup, RelativeMorphism.Homotopy.h₁, stdSimplex.spineId_vertex, stdSimplex.objMk₁_apply_eq_zero_iff, RelativeMorphism.Homotopy.postcomp_h, stdSimplex.σ_objMk₁_of_lt, stdSimplex.face_inter_face, stdSimplex.mem_nonDegenerate_iff_mono, horn₃₂.desc.multicofork_pt, prodStdSimplex.strictMono_orderHomOfSimplex, horn₂₂.isPushout, prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, yonedaEquiv_comp, stdSimplex.spineId_arrow_apply_one, Quasicategory.hornFilling', RelativeMorphism.Homotopy.rel, horn.primitiveEdge_coe_down, stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, stdSimplex.face_le_face_iff, RelativeMorphism.Homotopy.refl_h, horn₃₁.ι₃_desc, PtSimplex.RelStruct.δ_succ_map, stdSimplex.δ_objMk₁_of_lt, ι₁_fst_assoc, stdSimplex.objMk₁_apply_eq_one_iff, stdSimplex.toSSetObj_app_const_one, horn.ι_ι_assoc, horn₃₂.desc.multicofork_π_zero, stdSimplex.objEquiv_symm_apply, horn₃₂.desc.multicofork_π_three_assoc, horn₃₂.desc.multicofork_π_one_assoc, KanComplex.hornFilling, PtSimplex.RelStruct.δ_map_of_gt, stdSimplex.nonDegenerateEquiv_symm_apply_coe, horn.ι_ι, horn₃₁.ι₀_desc, PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, horn.const_val_apply, horn₃₁.desc.multicofork_π_three, horn₃₂.ι₃_desc_assoc, horn₂₁.sq, horn.primitiveTriangle_coe, stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ, stdSimplex.face_singleton_compl, ι₀_app_fst, horn₃₂.ι₀_desc_assoc, stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc, ι₁_comp_assoc, PtSimplex.RelStruct.δ_succ_map_assoc, stdSimplex.isoNerve_inv_app_apply, PtSimplex.MulStruct.δ_castSucc_castSucc_map, RelativeMorphism.Homotopy.rel_assoc
yonedaEquiv 📖	CompOp	11 math math: Subcomplex.range_eq_ofSimplex, horn.yonedaEquiv_ι, yonedaEquiv_symm_zero, Subcomplex.ofSimplexProd_eq_range, yonedaEquiv_symm_comp, Subcomplex.yonedaEquiv_coe, stdSimplex.yonedaEquiv_symm_app_objEquiv_symm, yonedaEquiv_const, stdSimplex.yonedaEquiv_map, stdSimplex.ofSimplex_yonedaEquiv_δ, yonedaEquiv_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
yonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj stdSimplex Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app	—	—
yonedaEquiv_const 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj stdSimplex Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv const	—	SimplexCategory.const_eq_id CategoryTheory.FunctorToTypes.map_id_apply
yonedaEquiv_symm_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj stdSimplex DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv CategoryTheory.NatTrans.app	—	CategoryTheory.uliftYonedaEquiv_symm_comp
yonedaEquiv_symm_zero 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category stdSimplex EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv const	—	Equiv.injective Equiv.apply_symm_apply yonedaEquiv_const

SSet.Augmented

Definitions

Name	Category	Theorems
stdSimplex 📖	CompOp	6 math math: stdSimplex_map_right, stdSimplex_obj_left, StandardSimplex.nonempty_extraDegeneracy_stdSimplex, stdSimplex_obj_right, stdSimplex_obj_hom_app, stdSimplex_map_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stdSimplex_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.SimplicialObject CategoryTheory.types CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj SSet SSet.stdSimplex CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from CategoryTheory.Functor.map SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented stdSimplex	—	—
stdSimplex_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.types CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj SSet SSet.stdSimplex CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from CategoryTheory.Functor.map SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented stdSimplex CategoryTheory.Comma.right	—	—
stdSimplex_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.Functor.category CategoryTheory.Functor.id SSet SSet.stdSimplex CategoryTheory.SimplicialObject.const CategoryTheory.Limits.terminal CategoryTheory.Comma.hom SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented stdSimplex CategoryTheory.Limits.terminal.from	—	—
stdSimplex_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.types CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented stdSimplex SSet SSet.stdSimplex	—	—
stdSimplex_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.types CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj SSet.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented stdSimplex CategoryTheory.Limits.terminal	—	—

SSet.Subcomplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_eq_ofSimplex 📖	mathematical	—	range CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet.stdSimplex ofSimplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op EquivLike.toFunLike Equiv.instEquivLike SSet.yonedaEquiv	—	CategoryTheory.Subfunctor.range_eq_ofSection'
yonedaEquiv_coe 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj DFunLike.coe Equiv Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category SSet.stdSimplex CategoryTheory.Subfunctor.toFunctor Set.Elem toSSet EquivLike.toFunLike Equiv.instEquivLike SSet.yonedaEquiv CategoryTheory.CategoryStruct.comp ι	—	—

SSet.stdSimplex

Definitions

Name	Category	Theorems
asOrderHom 📖	CompOp	1 math math: SSet.horn_obj
const 📖	CompOp	5 math math: obj₀Equiv_symm_apply, toSSetObj_app_const_zero, const_down_toOrderHom, SSet.horn.spineId_vertex_coe, toSSetObj_app_const_one
edge 📖	CompOp	2 math math: coe_edge_down_toOrderHom, SSet.horn.edge_coe
face 📖	CompOp	40 math math: SSet.horn₃₁.desc.multicofork_π_two, SSet.horn.faceSingletonComplIso_inv_ι_assoc, faceSingletonIso_zero_hom_comp_ι_eq_δ, SSet.horn₃₂.desc.multicofork_π_one, SSet.horn₂₂.sq, face_eq_ofSimplex, SSet.horn₃₁.desc.multicofork_pt, SSet.horn.faceSingletonComplIso_inv_ι, range_δ, faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.horn₃₁.desc.multicofork_π_zero_assoc, face_obj, SSet.horn₂₀.sq, mem_face_iff, faceSingletonIso_one_hom_comp_ι_eq_δ, faceSingletonComplIso_hom_ι, SSet.face_le_horn, SSet.horn.faceι_ι, SSet.horn_eq_iSup, obj₀Equiv_symm_mem_face_iff, SSet.horn₃₂.desc.multicofork_π_zero_assoc, SSet.horn.faceι_ι_assoc, SSet.horn.multicoequalizerDiagram, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.horn₃₁.desc.multicofork_π_zero, ofSimplex_yonedaEquiv_δ, SSet.horn₃₂.desc.multicofork_π_three, faceSingletonComplIso_hom_ι_assoc, SSet.boundary_eq_iSup, face_inter_face, SSet.horn₃₂.desc.multicofork_pt, faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, face_le_face_iff, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, SSet.horn₃₁.desc.multicofork_π_three, SSet.horn₂₁.sq, face_singleton_compl
facePairIso 📖	CompOp	—
faceRepresentableBy 📖	CompOp	—
faceSingletonComplIso 📖	CompOp	16 math math: SSet.horn₃₁.desc.multicofork_π_two, SSet.horn.faceSingletonComplIso_inv_ι_assoc, SSet.horn₃₂.desc.multicofork_π_one, SSet.horn.faceSingletonComplIso_inv_ι, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.horn₃₁.desc.multicofork_π_zero_assoc, faceSingletonComplIso_hom_ι, SSet.horn₃₂.desc.multicofork_π_zero_assoc, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.horn₃₁.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three, faceSingletonComplIso_hom_ι_assoc, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, SSet.horn₃₁.desc.multicofork_π_three
faceSingletonIso 📖	CompOp	4 math math: faceSingletonIso_zero_hom_comp_ι_eq_δ, faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, faceSingletonIso_one_hom_comp_ι_eq_δ, faceSingletonIso_one_hom_comp_ι_eq_δ_assoc
finSuccAboveOrderIsoFinset 📖	CompOp	—
instDecidableEqHomObjSimplexCategoryOfOppositeOp 📖	CompOp	—
instDecidableEqObjOppositeSimplexCategory 📖	CompOp	—
instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat 📖	CompOp	24 math math: mem_nonDegenerate_iff_strictMono, SSet.prodStdSimplex.orderHomOfSimplex_coe, SSet.prodStdSimplex.objEquiv_apply_fst, ext_iff, obj₀Equiv_apply, spineId_arrow_apply_zero, objMk₁_apply, SSet.prodStdSimplex.objEquiv_apply_snd, SSet.ι₁_app_snd_apply, nonDegenerateEquiv_apply_apply, mem_face_iff, isoNerve_hom_app_apply, objMk₁_of_castSucc_lt, objMk₁_of_le_castSucc, monotone_apply, objEquiv_toOrderHom_apply, SSet.ι₀_app_snd_apply, objMk_apply, objMk₁_apply_eq_zero_iff, spineId_arrow_apply_one, objMk₁_apply_eq_one_iff, objEquiv_symm_apply, SSet.horn.const_val_apply, isoNerve_inv_app_apply
isoNerve 📖	CompOp	2 math math: isoNerve_hom_app_apply, isoNerve_inv_app_apply
isoOfRepresentableBy 📖	CompOp	—
nonDegenerateEquiv 📖	CompOp	2 math math: nonDegenerateEquiv_apply_apply, nonDegenerateEquiv_symm_apply_coe
objEquiv 📖	CompOp	14 math math: δ_objEquiv_symm_apply, face_obj, map_apply, yonedaEquiv_symm_app_objEquiv_symm, σ_objEquiv_symm_apply, objEquiv_symm_mem_nonDegenerate_iff_mono, SSet.prodStdSimplex.nonDegenerateEquiv₁_fst, objEquiv_symm_comp, yonedaEquiv_map, objEquiv_toOrderHom_apply, mem_nonDegenerate_iff_mono, objEquiv_symm_apply, nonDegenerateEquiv_symm_apply_coe, face_singleton_compl
objMk 📖	CompOp	3 math math: objMk_bijective, face_eq_ofSimplex, objMk_apply
obj₀Equiv 📖	CompOp	10 math math: δ_zero_eq_const, SSet.ι₀_snd_assoc, obj₀Equiv_symm_apply, obj₀Equiv_apply, SSet.ι₀_snd, SSet.ι₁_snd_assoc, SSet.ι₁_snd, obj₀Equiv_symm_mem_face_iff, δ_one_eq_const, spineId_vertex
triangle 📖	CompOp	2 math math: coe_triangle_down_toOrderHom, SSet.horn.primitiveTriangle_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_edge_down_toOrderHom 📖	mathematical	—	DFunLike.coe OrderHom SimplexCategory.len Opposite.unop SimplexCategory Opposite.op PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda edge Matrix.vecCons Matrix.vecEmpty	—	—
coe_triangle_down_toOrderHom 📖	mathematical	—	DFunLike.coe OrderHom SimplexCategory.len Opposite.unop SimplexCategory Opposite.op PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda triangle Matrix.vecCons Matrix.vecEmpty	—	—
const_down_toOrderHom 📖	mathematical	—	SimplexCategory.Hom.toOrderHom Opposite.unop SimplexCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda const DFunLike.coe OrderHom SimplexCategory.len PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instPreorder OrderHom.instFunLike OrderHom.const	—	—
ext 📖	—	DFunLike.coe CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	—	DFunLike.ext
ext_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	—	ext
faceSingletonComplIso_hom_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex SSet.Subcomplex.toSSet face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton CategoryTheory.Iso.hom faceSingletonComplIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	—
faceSingletonComplIso_hom_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex SSet.Subcomplex.toSSet face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton CategoryTheory.Iso.hom faceSingletonComplIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' faceSingletonComplIso_hom_ι
faceSingletonIso_one_hom_comp_ι_eq_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex SSet.Subcomplex.toSSet face Finset Finset.instSingleton CategoryTheory.Iso.hom faceSingletonIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	—
faceSingletonIso_one_hom_comp_ι_eq_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex SSet.Subcomplex.toSSet face Finset Finset.instSingleton CategoryTheory.Iso.hom faceSingletonIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' faceSingletonIso_one_hom_comp_ι_eq_δ
faceSingletonIso_zero_hom_comp_ι_eq_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex SSet.Subcomplex.toSSet face Finset Finset.instSingleton CategoryTheory.Iso.hom faceSingletonIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	—
faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex SSet.Subcomplex.toSSet face Finset Finset.instSingleton CategoryTheory.Iso.hom faceSingletonIso SSet.Subcomplex.ι CategoryTheory.CosimplicialObject.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' faceSingletonIso_zero_hom_comp_ι_eq_δ
face_eq_ofSimplex 📖	mathematical	—	face SSet.Subcomplex.ofSimplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet.stdSimplex objMk Opposite.op OrderHom.comp SimplexCategory.len Opposite.unop Finset SetLike.instMembership Finset.instSetLike PartialOrder.toPreorder Fin.instPartialOrder Subtype.preorder OrderHom.Subtype.val OrderEmbedding.toOrderHom OrderIso.toOrderEmbedding	—	le_antisymm mem_face_iff OrderHom.monotone ext OrderIso.apply_symm_apply
face_inter_face 📖	mathematical	—	SSet.Subcomplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet.stdSimplex SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor face Finset Finset.instLattice	—	CategoryTheory.Subfunctor.ext Set.ext
face_le_face_iff 📖	mathematical	—	SSet.Subcomplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet.stdSimplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor face Finset Finset.partialOrder	—	obj₀Equiv_symm_mem_face_iff LE.le.trans
face_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj SSet CategoryTheory.Functor.category CategoryTheory.types SSet.stdSimplex face setOf Finset SimplexCategory.len Preorder.toLE PartialOrder.toPreorder Finset.partialOrder Finset.image Opposite.unop DFunLike.coe OrderHom Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike objEquiv Top.top BooleanAlgebra.toTop Finset.booleanAlgebra SimplexCategory.instFintypeToTypeOrderHomFinHAddNatLenOfNat	—	—
face_singleton_compl 📖	mathematical	—	face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton SSet.Subcomplex.ofSimplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet.stdSimplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm objEquiv SimplexCategory.δ	—	face_eq_ofSimplex
instFiniteObjOppositeSimplexCategory 📖	mathematical	—	Finite CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex	—	Equiv.finite_iff SimplexCategory.instFiniteHom
instFiniteObjSimplexCategory 📖	mathematical	—	SSet.Finite CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet.stdSimplex	—	SSet.finite_of_hasDimensionLT instHasDimensionLEObjSimplexCategoryMk Subtype.finite instFiniteObjOppositeSimplexCategory
instFiniteToSSetOfSimplex 📖	mathematical	—	SSet.Finite SSet.Subcomplex.toSSet SSet.Subcomplex.ofSimplex	—	Equiv.surjective SSet.Subcomplex.range_eq_ofSimplex SSet.finite_range instFiniteObjSimplexCategory
instHasDimensionLEObjSimplexCategoryMk 📖	mathematical	—	SSet.HasDimensionLE CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet.stdSimplex	—	Set.ext mem_nonDegenerate_iff_mono SimplexCategory.len_le_of_mono
isoNerve_hom_app_apply 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory.len Opposite.unop SimplexCategory Opposite.op Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ULift.instPreorder CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex CategoryTheory.nerve CategoryTheory.Iso.hom isoNerve DFunLike.coe instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	—
isoNerve_inv_app_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 CategoryTheory.NatTrans.app CategoryTheory.nerve Preorder.smallCategory ULift.instPreorder PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Iso.inv isoNerve SimplexCategory.len Opposite.unop	—	—
map_apply 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet CategoryTheory.Functor.category SSet.stdSimplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop EquivLike.toFunLike Equiv.instEquivLike Equiv.symm objEquiv CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	—
map_id 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet.stdSimplex OrderHom.id SimplexCategory.len PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_id
mem_face_iff 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj face Finset SetLike.instMembership Finset.instSetLike DFunLike.coe instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	—
mem_nonDegenerate_iff_mono 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op Set Set.instMembership SSet.nonDegenerate CategoryTheory.Mono Opposite.unop DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike objEquiv	—	mem_nonDegenerate_iff_strictMono SimplexCategory.mono_iff_injective StrictMono.injective Fin.strictMono_iff_lt_succ LE.le.lt_or_eq monotone_apply Fin.castSucc_le_succ
mem_nonDegenerate_iff_strictMono 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op Set Set.instMembership SSet.nonDegenerate StrictMono PartialOrder.toPreorder Fin.instPartialOrder DFunLike.coe instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	SSet.nonDegenerate_iff_of_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom PartialOrder.mem_nerve_nonDegenerate_iff_strictMono
monotone_apply 📖	mathematical	—	Monotone PartialOrder.toPreorder Fin.instPartialOrder DFunLike.coe CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	OrderHom.monotone
nonDegenerateEquiv_apply_apply 📖	mathematical	—	DFunLike.coe RelEmbedding Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Fin.instLinearOrder Fin.instPartialOrder RelEmbedding.instFunLike Equiv Set.Elem CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op SSet.nonDegenerate OrderEmbedding EquivLike.toFunLike Equiv.instEquivLike nonDegenerateEquiv instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat Set Set.instMembership	—	—
nonDegenerateEquiv_symm_apply_coe 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op Set Set.instMembership SSet.nonDegenerate DFunLike.coe Equiv OrderEmbedding Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm nonDegenerateEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop objEquiv OrderEmbedding.toOrderHom PartialOrder.toPreorder Fin.instPartialOrder	—	—
objEquiv_symm_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 Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop EquivLike.toFunLike Equiv.instEquivLike Equiv.symm objEquiv OrderHom SimplexCategory.len PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom	—	—
objEquiv_symm_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SimplexCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex EquivLike.toFunLike Equiv.instEquivLike Equiv.symm objEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	—
objEquiv_symm_mem_nonDegenerate_iff_mono 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op Set Set.instMembership SSet.nonDegenerate DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop EquivLike.toFunLike Equiv.instEquivLike Equiv.symm objEquiv CategoryTheory.Mono	—	Equiv.apply_symm_apply
objEquiv_toOrderHom_apply 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom Equiv CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike objEquiv instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	—
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 OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike	—	—
objMk_bijective 📖	mathematical	—	Function.Bijective OrderHom SimplexCategory.len Opposite.unop SimplexCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex objMk	—	Equiv.bijective
obj₀Equiv_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op EquivLike.toFunLike Equiv.instEquivLike obj₀Equiv instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat	—	—
obj₀Equiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm obj₀Equiv const	—	—
obj₀Equiv_symm_mem_face_iff 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet CategoryTheory.Functor.category SSet.stdSimplex Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj face DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm obj₀Equiv Finset SetLike.instMembership Finset.instSetLike	—	—
ofSimplex_yonedaEquiv_δ 📖	mathematical	—	SSet.Subcomplex.ofSimplex CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet.stdSimplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op EquivLike.toFunLike Equiv.instEquivLike SSet.yonedaEquiv CategoryTheory.CosimplicialObject.δ face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton	—	face_eq_ofSimplex
range_δ 📖	mathematical	—	SSet.Subcomplex.range CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite CategoryTheory.types SSet.stdSimplex CategoryTheory.CosimplicialObject.δ face Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype Finset.instSingleton	—	SSet.Subcomplex.range_eq_ofSimplex ofSimplex_yonedaEquiv_δ
yonedaEquiv_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex Opposite.op EquivLike.toFunLike Equiv.instEquivLike SSet.yonedaEquiv CategoryTheory.Functor.map Opposite.unop Equiv.symm objEquiv	—	Equiv.injective
yonedaEquiv_symm_app_objEquiv_symm 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet CategoryTheory.Functor.category SSet.stdSimplex DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm SSet.yonedaEquiv Opposite.unop objEquiv CategoryTheory.Functor.map Quiver.Hom.op	—	—
δ_objEquiv_symm_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite SSet.stdSimplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op EquivLike.toFunLike Opposite.unop Equiv.instEquivLike Equiv.symm objEquiv CategoryTheory.CategoryStruct.comp SimplexCategory.δ	—	—
δ_one_eq_const 📖	mathematical	—	CategoryTheory.CosimplicialObject.δ SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet.stdSimplex SSet.const CategoryTheory.Functor.obj DFunLike.coe Equiv Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm obj₀Equiv	—	—
δ_zero_eq_const 📖	mathematical	—	CategoryTheory.CosimplicialObject.δ SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet.stdSimplex SSet.const CategoryTheory.Functor.obj DFunLike.coe Equiv Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm obj₀Equiv	—	—
σ_objEquiv_symm_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.σ CategoryTheory.types CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet CategoryTheory.Functor.category Opposite CategoryTheory.Category.opposite SSet.stdSimplex DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op EquivLike.toFunLike Opposite.unop Equiv.instEquivLike Equiv.symm objEquiv CategoryTheory.CategoryStruct.comp SimplexCategory.σ	—	—

Simplicial

Definitions

Name	Category	Theorems
«termΔ[_]» 📖	CompOp	—

---

← Back to Index