Mathlib Map

Theorems · Definition · algebraic topology

SSet.S.subcomplex

{X : SSet} → X.S → X.Subcomplex

The subcomplex generated by a simplex.

Defined in
Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Cited by
39 results in Mathlib
Foundations
Depth 35 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SSet.Subcomplex.Pairing.RankFunction.filtration · cited by 34RankFunction.filtrationSSet.Subcomplex.Pairing.RankFunction.filtration_monotone · cited by 8RankFunction.filtration_m…SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration · cited by 6RankFunction.subcomplex_l…SSet.Subcomplex.Pairing.RankFunction.filtration_def · cited by 4RankFunction.filtration_d…SSet.N.le_iff_exists_mono · cited by 3N.le_iff_exists_monoSSet.Subcomplex.Pairing.RankFunction.filtration_bot · cited by 3RankFunction.filtration_b…SSet.S.le_def · cited by 3S.le_defSSet.Subcomplex.Pairing.RankFunction.Cell.range_map · cited by 2Cell.range_mapSSet.Subcomplex.Pairing.RankFunction.Cell.subcomplex_not_le_image_horn · cited by 2Cell.subcomplex_not_le_im…SSet.N.le_iff · cited by 2N.le_iffSSet.S.IsUniquelyCodimOneFace.le · cited by 2IsUniquelyCodimOneFace.leSSet.N.subcomplex_injective · cited by 2N.subcomplex_injectiveSSet.N.subcomplex_le_iff · cited by 2N.subcomplex_le_iffSSet.S.existsUnique_n · cited by 2S.existsUnique_nSSet.S.le_iff · cited by 2S.le_iffSSet · cited by 1283SSetSSet.Subcomplex · cited by 461SSet.SubcomplexSSet.S.simplex · cited by 111S.simplexSSet.Subcomplex.ofSimplex · cited by 73Subcomplex.ofSimplexSSet.S · cited by 69SSet.SS.subcomplexCITED BYCITES

Cites5

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

Cited by41

Results whose statement or proof uses this declaration.