English
If i.castSucc < j, then the i-th vertex of the spine of the j-th face of spineToSimplex f equals the (i.castSucc)-th vertex of f.
Русский
Если i.castSucc < j, то i-я вершина спайна лица j-ного в spineToSimplex f равна i.castSucc-й вершине f.
LaTeX
$$$$ (X.spine\ n (X.δ j (sx.spineToSimplex f))).vertex i = f.vertex i.castSucc $$$$
Lean4
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
the common vertices will agree with those of the original path `f`. In particular,
a vertex `i` with `i < j` can be identified with the same vertex in `f`. -/
theorem spine_δ_vertex_lt (h : i.castSucc < j) :
(X.spine n (X.δ j (sx.spineToSimplex f))).vertex i = f.vertex i.castSucc :=
by
simp only [SimplicialObject.δ, spine_vertex]
rw [← FunctorToTypes.map_comp_apply, ← op_comp, SimplexCategory.const_comp, spineToSimplex_vertex]
simp only [SimplexCategory.δ, Hom.toOrderHom, len_mk, mkHom, Hom.mk, OrderEmbedding.toOrderHom_coe,
Fin.succAboveOrderEmb_apply]
rw [Fin.succAbove_of_castSucc_lt j i h]
