vertex — Mathlib

English

A path includes the data of n+1 0-simplices; the vertex function extracts these 0-simplices.

Русский

Путь содержит данные о n+1 нулевых (0) симплексах; функция вершины извлекает их.

LaTeX

$$$\\text{vertex}(f,i) : X_{0} \\quad( i\\in \\{0,\\dots,n\\} )$$$

Lean4

/-- A path includes the data of `n + 1` 0-simplices in `X`. -/
abbrev vertex (f : Path X n) (i : Fin (n + 1)) : X _⦋0⦌ :=
  Truncated.Path.vertex f i

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