vertex — Mathlib

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⟩

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