Simplices

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

Statistics

Metric	Count
Definitions S, cast, dim, equivElements, instPreorder, map, simplex, subcomplex	8
Theorems cast_dim, cast_eq_self, cast_simplex_rfl, dim_eq_of_eq, dim_eq_of_mk_eq, equivElements_apply_fst, equivElements_apply_snd, equivElements_symm_apply_dim, equivElements_symm_apply_simplex, ext_iff, ext_iff', le_def, le_iff, le_iff_nonempty_hom, mk_map_eq_iff_of_mono, mk_map_le, mk_surjective	17
Total	25

SSet

Definitions

Name	Category	Theorems
S 📖	CompData	8 math math: S.equivElements_symm_apply_dim, S.le_iff, S.equivElements_apply_fst, S.equivElements_apply_snd, S.le_iff_nonempty_hom, S.equivElements_symm_apply_simplex, S.mk_map_le, S.le_def

SSet.S

Definitions

Name	Category	Theorems
cast 📖	CompOp	8 math math: cast_dim, cast_simplex_rfl, ext_iff', IsUniquelyCodimOneFace.cast, IsUniquelyCodimOneFace.δ_eq_iff, IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex, IsUniquelyCodimOneFace.δ_index, cast_eq_self
dim 📖	CompOp	20 math math: SSet.iSup_subcomplexOfSimplex_prod_eq_top, SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index, equivElements_symm_apply_dim, SSet.Subcomplex.Pairing.dim_p, cast_simplex_rfl, SSet.N.dim_le_of_le, le_iff, SSet.N.mk_dim, IsUniquelyCodimOneFace.dim_eq, SSet.N.dim_lt_of_lt, SSet.Subcomplex.PairingCore.type₂_dim, ext_iff', equivElements_apply_fst, SSet.N.le_iff_exists_mono, SSet.Subcomplex.Pairing.AncestralRel.dim_le, SSet.Subcomplex.PairingCore.type₁_dim, SSet.N.nonDegenerate, dim_eq_of_eq, SSet.Subcomplex.N.mk_dim, SSet.Subcomplex.N.notMem
equivElements 📖	CompOp	5 math math: equivElements_symm_apply_dim, equivElements_apply_fst, equivElements_apply_snd, le_iff_nonempty_hom, equivElements_symm_apply_simplex
instPreorder 📖	CompOp	4 math math: le_iff, le_iff_nonempty_hom, mk_map_le, le_def
map 📖	CompOp	—
simplex 📖	CompOp	16 math math: SSet.iSup_subcomplexOfSimplex_prod_eq_top, cast_simplex_rfl, le_iff, ext_iff', SSet.Subcomplex.PairingCore.type₂_simplex, SSet.N.le_iff_exists_mono, SSet.N.mk_simplex, equivElements_apply_snd, equivElements_symm_apply_simplex, SSet.N.nonDegenerate, IsUniquelyCodimOneFace.δ_eq_iff, SSet.Subcomplex.PairingCore.type₁_simplex, IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex, SSet.Subcomplex.N.mk_simplex, SSet.Subcomplex.N.notMem, IsUniquelyCodimOneFace.δ_index
subcomplex 📖	CompOp	9 math math: SSet.orderEmbeddingN_apply, SSet.N.subcomplex_injective_iff, SSet.N.le_iff, toN_eq_iff, SSet.N.eq_iff, SSet.N.iSup_subcomplex_eq_top, subcomplex_toN, le_def, existsUnique_n

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_dim 📖	mathematical	dim	cast	—	—
cast_eq_self 📖	mathematical	dim	cast	—	mk_surjective
cast_simplex_rfl 📖	mathematical	—	simplex cast dim	—	—
dim_eq_of_eq 📖	mathematical	—	dim	—	—
dim_eq_of_mk_eq 📖	—	—	—	—	dim_eq_of_eq
equivElements_apply_fst 📖	mathematical	—	Opposite SimplexCategory CategoryTheory.Functor.obj CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types DFunLike.coe Equiv SSet.S CategoryTheory.Functor.Elements EquivLike.toFunLike Equiv.instEquivLike equivElements Opposite.op dim	—	—
equivElements_apply_snd 📖	mathematical	—	Opposite SimplexCategory CategoryTheory.Functor.obj CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types DFunLike.coe Equiv SSet.S CategoryTheory.Functor.Elements EquivLike.toFunLike Equiv.instEquivLike equivElements simplex	—	—
equivElements_symm_apply_dim 📖	mathematical	—	dim DFunLike.coe Equiv CategoryTheory.Functor.Elements Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory SSet.S EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivElements SimplexCategory.len Opposite.unop	—	—
equivElements_symm_apply_simplex 📖	mathematical	—	simplex DFunLike.coe Equiv CategoryTheory.Functor.Elements Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory SSet.S EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivElements CategoryTheory.Functor.obj CategoryTheory.types	—	—
ext_iff 📖	—	—	—	—	—
ext_iff' 📖	mathematical	—	simplex cast dim	—	mk_surjective
le_def 📖	mathematical	—	SSet.S Preorder.toLE instPreorder SSet.Subcomplex PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory subcomplex	—	—
le_iff 📖	mathematical	—	SSet.S Preorder.toLE instPreorder CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op dim Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct simplex	—	le_def SSet.Subcomplex.ofSimplex_le_iff CategoryTheory.Subfunctor.ofSection_obj Set.mem_setOf_eq
le_iff_nonempty_hom 📖	mathematical	—	SSet.S Preorder.toLE instPreorder Quiver.Hom CategoryTheory.Functor.Elements Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.categoryOfElements DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivElements	—	le_iff
mk_map_eq_iff_of_mono 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.IsIso	—	CategoryTheory.IsIso.id SimplexCategory.eq_id_of_mono dim_eq_of_mk_eq CategoryTheory.FunctorToTypes.map_id_apply SimplexCategory.eq_id_of_isIso SimplexCategory.eq_of_isIso
mk_map_le 📖	mathematical	—	SSet.S Preorder.toLE instPreorder CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	le_iff
mk_surjective 📖	—	—	—	—	—

---

← Back to Index