spineId_arrow_apply_zero — Mathlib

English

The i-th edge of spineId n at position 0 equals i.castSucc, i.e., the 0-th face maps to the successor vertex.

Русский

i-е ребро spineId n на положении 0 равно i.castSucc, то есть 0-я грань переходит к следующей вершине.

LaTeX

$$$(\mathrm{stdSimplex.spineId}(n)).arrow i\, 0 = i.castSucc$$$

Lean4

@[simp]
theorem spineId_arrow_apply_zero (n : ℕ) (i : Fin n) : (stdSimplex.spineId n).arrow i 0 = i.castSucc :=
  rfl

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