spine_map_subinterval — Mathlib

English

Truncating above a subinterval corresponds to taking the subinterval of the spine data.

Русский

Усечение выше подинтервала соответствует выборке подинтервала по данным позвоночника.

LaTeX

$$$\\text{spine\_map\_subinterval}(X,m,k)(\\Delta) = \\Delta_{[j,l]}$$$

Lean4

theorem spine_map_subinterval (j l : ℕ) (h : j + l ≤ m) (Δ : X _⦋m⦌ₙ ₊ ₁) :
    X.spine l (by cutsat) (X.map (tr (subinterval j l h)).op Δ) = (X.spine m hₘ Δ).interval j l h :=
  by
  ext i
  · dsimp only [spine_vertex, Path.interval]
    rw [← FunctorToTypes.map_comp_apply, ← op_comp, ← tr_comp, const_subinterval_eq]
  · dsimp only [spine_arrow, Path.interval]
    rw [← FunctorToTypes.map_comp_apply, ← op_comp, ← tr_comp, mkOfSucc_subinterval_eq]

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