spineToSimplex_arrow — Mathlib

English

The spineEquiv respects arrows, i.e., the correspondence between arrows in X via the spine and the path arrows matches.

Русский

SpineEquiv сохраняет стрелки; соответствие между стрелками в X через spine и стрелками путей совпадает.

LaTeX

$$spineEquiv.morphism respects arrows: spineEquiv.map( f.arrow i ) = f.arrow i$$

Lean4

@[simp]
theorem spineToSimplex_arrow (i : Fin n) (f : Path X n) : X.map (mkOfSucc i).op (sx.spineToSimplex f) = f.arrow i := by
  rw [← spine_arrow, spine_spineToSimplex_apply]

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