English
If j ≤ i.castSucc, then the i-th vertex of the spine of δ_j(sx.spineToSimplex f) equals the (i.castSucc)-th vertex of f.
Русский
Если j ≤ i.castSucc, то i-я вершина спайна δ_j( sx.spineToSimplex f ) равна вершине f с индексом i.castSucc.
LaTeX
$$$$ (X.spine n (X.\delta j (sx.spineToSimplex f))).vertex i = f.vertex i.succ $$$$
Lean4
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
a vertex `i` with `i ≥ j` can be identified with vertex `i + 1` in the original
path. -/
theorem spine_δ_vertex_ge (h : j ≤ i.castSucc) : (X.spine n (X.δ j (sx.spineToSimplex f))).vertex i = f.vertex i.succ :=
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_le_castSucc j i h]
