vertex_coe

Mathlib.Analysis.Convex.StdSimplex

URI: https://scilib.ai/kg/mathlib#stdSimplex.vertex_coe

English

The function component of a vertex coincides with the singleton coordinate vector.

Русский

Компонента функции вершины совпадает с вектором-одиночкой координат.

LaTeX

$$$\forall x, \operatorname{vertex}(x) = \Pi\text{single}(x,1)$$$

Lean4

@[simp]
theorem vertex_coe [DecidableEq X] (x : X) : ⇑(vertex (S := S) x) = Pi.single x 1 :=
  rfl

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

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

Разделы

Аффилиация

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