English
Spine commutes with taking subintervals: the spine of a mapped n-simplex over a subinterval equals the interval of the spine of the original over that subinterval.
Русский
Хребет коммутирует взятие подотрезков: хребет образованного n-симплекса по подотрезку равен интервалу хребета исходного по тому подотрезку.
LaTeX
$$$X.spine l (X.map (subinterval j l h).op Δ) = (X.spine n Δ).interval j l h$$$
Lean4
theorem spine_map_subinterval (j l : ℕ) (h : j + l ≤ n) (Δ : X _⦋n⦌) :
X.spine l (X.map (subinterval j l h).op Δ) = (X.spine n Δ).interval j l h :=
truncation (n + 1) |>.obj X |>.spine_map_subinterval n (by cutsat) j l h Δ