spine_arrow — Mathlib

English

The i-th arrow of the spine of Δ is the image under the canonical face map that shifts by 1, i.e., (X.spine n Δ).arrow i = X.map (mkOfSucc i).op Δ.

Русский

i-й ребро хребта Δ получается как образ через отображение лица, смещающее индекс на 1: (X.spine n Δ).arrow i = X.map (mkOfSucc i).op Δ.

LaTeX

$$$(X.spine n \Delta).arrow i = X.map( (\mathrm{mkOfSucc}~i) ).op \Delta$$$

Lean4

@[simp]
theorem spine_arrow (Δ : X _⦋n⦌) (i : Fin n) : (X.spine n Δ).arrow i = X.map (mkOfSucc i).op Δ :=
  rfl

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