Mathlib Map

Theorems · Definition · algebraic topology

SSet.S.dim

{X : SSet} → X.S → ℕ

the dimension of the simplex

Defined in
Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Cited by
162 results in Mathlib
Foundations
Depth 33 from the axioms, rests on 271 definitions · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SSet.S.simplex · cited by 111S.simplexSSet.Subcomplex.Pairing.RankFunction.Cell.dim · cited by 40Cell.dimSSet.S.cast · cited by 35S.castSSet.Subcomplex.N.cast · cited by 33N.castSSet.prodStdSimplex.pairingCore.IsIndex · cited by 26pairingCore.IsIndexSSet.S.IsUniquelyCodimOneFace · cited by 19S.IsUniquelyCodimOneFaceSSet.prodStdSimplex.pairingCore.min · cited by 18pairingCore.minSSet.S.IsUniquelyCodimOneFace.index · cited by 14IsUniquelyCodimOneFace.in…SSet.prodStdSimplex.pairingCore.IsType₂.φ · cited by 14IsType₂.φSSet.prodStdSimplex.pairingCore.IsType₂ · cited by 14pairingCore.IsType₂SSet.N.nonDegenerate · cited by 11N.nonDegenerateSSet.N.monoOfLE · cited by 9N.monoOfLESSet.S.IsUniquelyCodimOneFace.δ_index · cited by 7IsUniquelyCodimOneFace.δ_…SSet.Subcomplex.N.notMem · cited by 7N.notMemSSet.prodStdSimplex.pairingCore.IsIndex.δ · cited by 7IsIndex.δSSet · cited by 1283SSetSSet.S · cited by 69SSet.SS.dimCITED BYCITES

Cites2

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.Sstatement and proof · cited by 69

Cited by212

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 212.