spineToSimplex_interval — Mathlib

English

Taking a subinterval j,l of length m corresponds to applying spineToSimplex to the interval of f.

Русский

Применение к подотрезку j,l соответствует применению spineToSimplex к интервалу f.

LaTeX

$$$X.map\bigl(tr\;\mathrm{subinterval}(j,l,hjl)\bigr)^{op}(\mathrm{spineToSimplex}(m,h,f)) = \mathrm{spineToSimplex}(l,\;\_,\;f.interval(j,l,hjl))$$$

Lean4

@[simp]
theorem spineToSimplex_interval (f : Path X m) (j l : ℕ) (hjl : j + l ≤ m) :
    X.map (tr (subinterval j l hjl)).op (sx.spineToSimplex m h f) = sx.spineToSimplex l _ (f.interval j l hjl) :=
  by
  apply sx.spineInjective l
  dsimp only [spineEquiv, Equiv.coe_fn_mk]
  rw [spine_spineToSimplex_apply]
  convert spine_map_subinterval X m h j l hjl <| sx.spineToSimplex m h f
  exact sx.spine_spineToSimplex_apply m h f |>.symm

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