Mathlib Map

Theorems · Definition · algebraic topology

SSet.Subcomplex.N.toN

{X : SSet} → {A : X.Subcomplex} → A.N → X.N
Defined in
Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Cited by
126 results in Mathlib
Foundations
Depth 34 from the axioms, rests on 274 definitions · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SSet.Subcomplex.Pairing.RankFunction.Cell.dim · cited by 40Cell.dimSSet.Subcomplex.Pairing.RankFunction.filtration · cited by 34RankFunction.filtrationSSet.Subcomplex.N.cast · cited by 33N.castSSet.prodStdSimplex.pairingCore.IsIndex · cited by 26pairingCore.IsIndexSSet.prodStdSimplex.pairingCore.min · cited by 18pairingCore.minSSet.prodStdSimplex.pairingCore.IsType₂.φ · cited by 14IsType₂.φSSet.prodStdSimplex.pairingCore.IsType₂ · cited by 14pairingCore.IsType₂SSet.Subcomplex.Pairing.RankFunction.Cell.map · cited by 12Cell.mapSSet.Subcomplex.Pairing.isUniquelyCodimOneFace · cited by 12Pairing.isUniquelyCodimOn…SSet.Subcomplex.Pairing.RankFunction.filtration_monotone · cited by 8RankFunction.filtration_m…SSet.Subcomplex.N.orderIsoOfIso · cited by 8N.orderIsoOfIsoSSet.prodStdSimplex.pairingCore.IsIndex.δ · cited by 7IsIndex.δSSet.prodStdSimplex.pairingCore.IsType₂.simplex · cited by 7IsType₂.simplexSSet.Subcomplex.N.notMem · cited by 7N.notMemSSet.prodStdSimplex.pairingCore.finset · cited by 7pairingCore.finsetSSet · cited by 1283SSetSSet.Subcomplex · cited by 461SSet.SubcomplexSSet.Subcomplex.N · cited by 155Subcomplex.NSSet.N · cited by 70SSet.NN.toNCITED BYCITES

Cites4

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

Cited by166

Results whose statement or proof uses this declaration.