English
The spine of an n-simplex in X is the length-n path obtained by traversing the vertices of the simplex in order, using the truncation at level n+1.
Русский
Хребет n-симплекса в X — это путь длины n, проходящий по вершинам симплекса в порядке обхода, с использованием усечения на уровне n+1.
LaTeX
$$$\mathrm{spine}(X,n) : X_{\langle n\rangle} \to \mathrm{Path}(X,n), \quad \mathrm{spine}(X,n) = \big(\operatorname{truncation}(n+1)\big)\text{.obj }X \;\mathrm{spine}~n$$$
Lean4
/-- The spine of an `n`-simplex in `X` is the path of edges of length `n` formed
by traversing in order through the vertices of `X _⦋n⦌ₙ₊₁`. -/
def spine : X _⦋n⦌ → Path X n :=
truncation (n + 1) |>.obj X |>.spine n
