Theorems · Definition · algebraic topology

SSet.Truncated.StrictSegal.spineToSimplex

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

The inverse to spine X m.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Cited by

14 results in Mathlib

Foundations

Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound