English
If i.succ.castSucc < j, then the i-th arrow of the spine of δ_j(sx.spineToSimplex f) equals the i.castSucc-th arrow of f.
Русский
Если i.succ.castSucc < j, то i-ая стрелка спайна δ_j( sx.spineToSimplex f ) равна i.castSucc-ой стрелке f.
LaTeX
$$$$ (X.spine n (X.\delta j (sx.spineToSimplex f))).arrow i = f.arrow i.castSucc $$$$
Lean4
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
the common arrows will agree with those of the original path `f`. In particular,
an arrow `i` with `i + 1 < j` can be identified with the same arrow in `f`. -/
theorem spine_δ_arrow_lt (h : i.succ.castSucc < j) :
(X.spine n (X.δ j (sx.spineToSimplex f))).arrow i = f.arrow i.castSucc :=
by
simp only [SimplicialObject.δ, spine_arrow]
rw [← FunctorToTypes.map_comp_apply, ← op_comp]
rw [mkOfSucc_δ_lt h, spineToSimplex_arrow]
