spineId_vertex — Mathlib

English

The i-th vertex of the spineId n lies at the i-th vertex under the standard vertex identification, i.e., it is the inverse image of i under the basic vertex equivalence.

Русский

i-я вершина хребта spineId n равна i-й вершине под стандартной идентификацией вершин; это образ противоположной карты вершин.

LaTeX

$$$(\mathrm{stdSimplex.spineId}(n)).vertex(i) = (\mathrm{obj}_0^{\mathrm{Equiv}})^{-1}(i)$$$

Lean4

@[simp]
theorem spineId_vertex (n : ℕ) (i : Fin (n + 1)) : (stdSimplex.spineId n).vertex i = obj₀Equiv.symm i :=
  rfl

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