spine_δ_arrow_eq — Mathlib

English

If j = i.succ.castSucc, the i-th spine arrow equals the i.succ-th arrow of the derived interval path.

Русский

Если j = i.succ.castSucc, i-я стрелка позвоночника равна i.succ-й стрелке полученного отрезка пути.

LaTeX

$$$ (X.spine m (X.map (tr (δ j)).op (sx.spineToSimplex (m+1) f))).arrow i = sx.spineToDiagonal 2 (\dots) (f.interval i 2 \dots)$$$

Lean4

theorem spine_δ_arrow_eq (hij : j = i.succ.castSucc) :
    (X.spine m _ (X.map (tr (δ j)).op (sx.spineToSimplex (m + 1) _ f))).arrow i =
      sx.spineToDiagonal 2 (by cutsat) (f.interval i 2 (by cutsat)) :=
  by rw [spine_arrow, ← FunctorToTypes.map_comp_apply, ← op_comp, ← tr_comp, mkOfSucc_δ_eq hij, spineToSimplex_edge]

Похожие утверждения