Mathlib Map

Theorems · Definition · algebraic topology

SSet.Subcomplex.Pairing.RankFunction.filtration

{X : SSet} →
  {A : X.Subcomplex} → {P : A.Pairing} → {ι : Type v} → [inst : LinearOrder ι] → P.RankFunction ι → ι → X.Subcomplex

The filtration of a simplicial set given by a rank function for a proper pairing of a subcomplex.

Defined in
Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Cited by
34 results in Mathlib
Foundations
Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LinearOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SSet.Subcomplex.Pairing.RankFunction.b · cited by 13RankFunction.bSSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc · cited by 9Cell.mapToSuccSSet.Subcomplex.Pairing.RankFunction.t · cited by 9RankFunction.tSSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn · cited by 8Cell.mapHornSSet.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.Subcomplex.Pairing.RankFunction.Cell.ι_b · cited by 3Cell.ι_bSSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_apply · cited by 3Cell.ι_b_app_applySSet.Subcomplex.Pairing.RankFunction.filtration_bot · cited by 3RankFunction.filtration_b…SSet.Subcomplex.Pairing.RankFunction.w · cited by 3RankFunction.wSSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc_ι · cited by 2Cell.mapToSucc_ιSSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app · cited by 2Cell.ι_b_appSSet.Subcomplex.Pairing.RankFunction.Cell.ι_t · cited by 2Cell.ι_tSSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app · cited by 2Cell.ι_t_appDFunLike.coe · cited by 62936DFunLike.coeLinearOrder · cited by 8572LinearOrderiSup · cited by 2415iSupSSet · cited by 1283SSetSSet.Subcomplex · cited by 461SSet.SubcomplexSSet.N.toS · cited by 171N.toSSSet.Subcomplex.N.toN · cited by 126N.toNSSet.Subcomplex.Pairing · cited by 117Subcomplex.PairingSSet.Subcomplex.Pairing.RankFunction · cited by 68Pairing.RankFunctionSSet.Subcomplex.Pairing.RankFunction.Cell · cited by 55RankFunction.CellSSet.S.subcomplex · cited by 39S.subcomplexSSet.Subcomplex.Pairing.p · cited by 32Pairing.pSSet.Subcomplex.Pairing.RankFunction.Cell.s · cited by 21Cell.sRankFunction.filtrationCITED BYCITES

Cites13

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

Cited by39

Results whose statement or proof uses this declaration.