Mathlib Map

Theorems · Definition · algebraic topology

SSet.Subcomplex.ofSimplex

{X : SSet} → {n : ℕ} → X.obj (Opposite.op { len := n }) → X.Subcomplex

The subcomplex of a simplicial set that is generated by a simplex.

Defined in
Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Cited by
73 results in Mathlib
Foundations
Depth 33 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SSet.PtSimplex · cited by 41SSet.PtSimplexSSet.S.subcomplex · cited by 39S.subcomplexSSet.skeleton · cited by 11SSet.skeletonSSet.Subcomplex.ofSimplex_le_iff · cited by 8Subcomplex.ofSimplex_le_i…SSet.RelativeMorphism.const · cited by 7RelativeMorphism.constSSet.Subcomplex.toOfSimplex · cited by 6Subcomplex.toOfSimplexSSet.stdSimplex.face_singleton_compl · cited by 6stdSimplex.face_singleton…SSet.Subcomplex.range_eq_ofSimplex · cited by 5Subcomplex.range_eq_ofSim…SSet.Subcomplex.mem_ofSimplex_obj · cited by 5Subcomplex.mem_ofSimplex_…SSet.mem_skeleton · cited by 4SSet.mem_skeletonSSet.relativeCellComplexOfMono.Cell.range_map_le · cited by 3Cell.range_map_leSSet.stdSimplex.face_eq_ofSimplex · cited by 3stdSimplex.face_eq_ofSimp…SSet.PtSimplex.relStructCastSuccEquivMulStruct · cited by 2PtSimplex.relStructCastSu…SSet.PtSimplex.relStructSuccEquivMulStruct · cited by 2PtSimplex.relStructSuccEq…SSet.Subcomplex.Pairing.RankFunction.Cell.range_map · cited by 2Cell.range_mapCategoryTheory.Functor.obj · cited by 19642Functor.objOpposite · cited by 8081OppositeSimplexCategory · cited by 2204SimplexCategorySSet · cited by 1283SSetSSet.Subcomplex · cited by 461SSet.SubcomplexCategoryTheory.Subfunctor.ofSection · cited by 14Subfunctor.ofSectionSubcomplex.ofSimplexCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by90

Results whose statement or proof uses this declaration.