spineToSimplex_interval — Mathlib

English

The interval map commutes with spineToSimplex, preserving subinterval structure of a path.

Русский

Интервалная карта коммутирует spineToSimplex, сохраняет структуру подпутьов.

LaTeX

$$X.map(subinterval j l hjl).op (sx.spineToSimplex f) = sx.spineToSimplex (f.interval j l hjl)$$

Lean4

@[simp]
theorem spineToSimplex_interval :
    X.map (subinterval j l hjl).op (sx.spineToSimplex f) = sx.spineToSimplex (f.interval j l hjl) :=
  by
  apply sx.spineInjective
  dsimp only [spineEquiv, Equiv.coe_fn_mk]
  rw [spine_spineToSimplex_apply, spine_map_subinterval, spine_spineToSimplex_apply]

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