Theorems · Definition · algebraic topology

SSet.Truncated.spine

{n : ℕ} →
  (X : SSet.Truncated (n + 1)) →
    (m : ℕ) →
      (h : autoParam (m ≤ n + 1) SSet.Truncated.spine._auto_1) →
        X.obj (Opposite.op { obj := { len := m }, property := h }) → X.Path m

The spine of an m-simplex in X is the path of edges of length m formed by traversing in order through its vertices.

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.Path
Cited by: 24 results in Mathlib
Foundations: Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites14

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

DFunLike.coeproof · cited by 62,936
CategoryTheory.Functor.objstatement and proof · cited by 19,642
CategoryTheory.Functor.mapproof · cited by 8,698
Oppositestatement · cited by 8,081
CategoryTheory.ConcreteCategory.homproof · cited by 4,022
SimplexCategorystatement · cited by 2,204
Quiver.Hom.opproof · cited by 1,948
SimplexCategory.lenstatement · cited by 542
SimplexCategory.Truncatedstatement · cited by 236
SSet.Truncatedstatement and proof · cited by 214
SimplexCategory.constproof · cited by 47
SimplexCategory.Truncated.Hom.trproof · cited by 43

Cited by35

Results whose statement or proof uses this declaration.

SSet.spineproof · cited by 23
SSet.Truncated.liftOfStrictSegal.f₂proof · cited by 8
SSet.Truncated.StrictSegal.spineEquivproof · cited by 6
SSet.Truncated.spine_arrowstatement · cited by 4
SSet.Truncated.StrictSegal.spine_spineToSimplex_applystatement · cited by 3
SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_oneproof · cited by 3
SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_zeroproof · cited by 3
SSet.Truncated.spine_vertexstatement · cited by 3
SSet.Truncated.IsStrictSegal.spine_bijectivestatement · cited by 2
SSet.Truncated.spine_map_subintervalstatement and proof · cited by 2
SSet.Truncated.StrictSegal.spineToSimplex_intervalproof · cited by 1
SSet.Truncated.StrictSegal.spineToSimplex_spinestatement · cited by 1