spineToSimplex_vertex — Mathlib

English

For any i in Fin(m+1), mapping the spineToSimplex image along the vertex i recovers the i-th vertex of the path f.

Русский

Для любого i в Fin(m+1) отображение вдоль вершины i восстанавливает i-ю вершину пути f.

LaTeX

$$$X.map\bigl(tr\;\mathrm{SimplexCategory.const}(0,m,i)\bigr)^{op}\bigl(\mathrm{spineToSimplex}(m,h,f)\bigr) = f.vertex(i)$$$

Lean4

@[simp]
theorem spineToSimplex_vertex (i : Fin (m + 1)) (f : Path X m) :
    X.map (tr (SimplexCategory.const ⦋0⦌ ⦋m⦌ i)).op (sx.spineToSimplex m h f) = f.vertex i := by
  rw [← spine_vertex, spine_spineToSimplex_apply]

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