English
If the vertex i is to the left of j in the δ-face, the i-th vertex of the spine along that face equals the i.castSucc-th vertex of f.
Русский
Если вершина i слева от j в δ-грани, то i-я вершина позвоночника вдоль этой грани равна i.castSucc-й вершине f.
LaTeX
$$$(X.spine m (X.map (tr (δ j)).op (sx.spineToSimplex (m+1) f))).vertex\,i = f.vertex\,i.castSucc$$$
Lean4
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
a vertex `i` with `j ≤ i` can be identified with vertex `i + 1` in the original
path. -/
theorem spine_δ_vertex_ge (hij : j ≤ i.castSucc) :
(X.spine m _ (X.map (tr (δ j)).op (sx.spineToSimplex (m + 1) _ f))).vertex i = f.vertex i.succ :=
by
rw [spine_vertex, ← FunctorToTypes.map_comp_apply, ← op_comp, ← tr_comp, SimplexCategory.const_comp,
spineToSimplex_vertex]
dsimp only [δ, len_mk, mkHom, Hom.toOrderHom_mk, Fin.succAboveOrderEmb_apply, OrderEmbedding.toOrderHom_coe]
rw [Fin.succAbove_of_le_castSucc j i hij]
