spineId_arrow_apply_one

Mathlib.AlgebraicTopology.SimplicialSet.Path

URI: https://scilib.ai/kg/mathlib#SSet.stdSimplex.spineId_arrow_apply_one

English

The i-th edge of spineId n at position 1 equals i.succ, i.e., the first face advances to the next vertex.

Русский

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

LaTeX

$$$(\mathrm{stdSimplex.spineId}(n)).arrow i\, 1 = i.succ$$$

Lean4

@[simp]
theorem spineId_arrow_apply_one (n : ℕ) (i : Fin n) : (stdSimplex.spineId n).arrow i 1 = i.succ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru