English
The vertex corresponding to an index x is represented by the function that assigns 1 to x and 0 elsewhere.
Русский
Вершина, соответствующая индексу x, задаётся функцией, которая даёт 1 на x и 0 в прочих местах.
LaTeX
$$$\operatorname{vertex}(x) = (\Pi\text{-single}(x,1), \text{proof})$$$
Lean4
/-- The vertex corresponding to `x : X` in `stdSimplex S X`. -/
abbrev vertex [DecidableEq X] (x : X) : stdSimplex S X :=
⟨Pi.single x 1, single_mem_stdSimplex S x⟩