spine_vertex — Mathlib

English

For a simplex Δ in X, the i-th vertex of its spine equals the i-th vertex of Δ mapped by the canonical vertex map.

Русский

Для симплекса Δ в X i-я вершина хребта равна i-й вершине Δ, отображённой каноническим отображением вершин.

LaTeX

$$$(X.spine n \Delta).vertex i = X.map( (\mathrm{const}_{0}^{(n)} ) i ).op \Delta$$$

Lean4

@[simp]
theorem spine_vertex (Δ : X _⦋n⦌) (i : Fin (n + 1)) :
    (X.spine n Δ).vertex i = X.map (SimplexCategory.const ⦋0⦌ ⦋n⦌ i).op Δ :=
  rfl

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