Theorems · Inductive type · algebraic topology
SSet.S
SSet → Type u
The type of simplices of a simplicial set X. This type X.S is in bijection
with X.Elements (see SSet.S.equivElements), but X.S is not what the literature
names "category of simplices of X", as the category on X.S comes from
a preorder (see S.le_iff_nonempty_hom).
- Cited by
- 69 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SSetstatement · cited by 1,283
Cited by98
Results whose statement or proof uses this declaration.
- SSet.N.toSstatement · cited by 171
- SSet.S.dimstatement and proof · cited by 162
- SSet.S.simplexstatement and proof · cited by 111
- SSet.S.subcomplexstatement and proof · cited by 39
- SSet.S.caststatement and proof · cited by 35
- SSet.S.IsUniquelyCodimOneFacestatement and proof · cited by 19
- SSet.S.IsUniquelyCodimOneFace.indexstatement and proof · cited by 14
- SSet.S.IsUniquelyCodimOneFace.δ_indexstatement and proof · cited by 7
- SSet.S.mk_surjectivestatement and proof · cited by 7
- SSet.N.ext_iffstatement · cited by 6
- SSet.S.IsUniquelyCodimOneFace.dim_eqstatement and proof · cited by 6
- SSet.S.toNstatement and proof · cited by 6