Mathlib Map

Theorems · Definition · algebraic topology

SSet.N.toS

{X : SSet} → X.N → X.S
Defined in
Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Cited by
171 results in Mathlib
Foundations
Depth 33 from the axioms, rests on 272 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.isUniquelyCodimOneFace · cited by 12Pairing.isUniquelyCodimOn…SSet.Subcomplex.Pairing.RankFunction.Cell.map · cited by 12Cell.mapSSet.N.nonDegenerate · cited by 11N.nonDegenerateSSet.N.monoOfLE · cited by 9N.monoOfLESSet.Subcomplex.Pairing.RankFunction.filtration_monotone · cited by 8RankFunction.filtration_m…SSet.Subcomplex.N.notMem · cited by 7N.notMemSSet.prodStdSimplex.pairingCore.IsIndex.δ · cited by 7IsIndex.δSSet.prodStdSimplex.pairingCore.IsType₂.simplex · cited by 7IsType₂.simplexSSet · cited by 1283SSetSSet.N · cited by 70SSet.NSSet.S · cited by 69SSet.SN.toSCITED BYCITES

Cites3

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

  • SSetstatement and proof · cited by 1,283
  • SSet.Nstatement and proof · cited by 70
  • SSet.Sstatement · cited by 69

Cited by225

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 225.