zero_le

Mathlib.Analysis.Convex.StdSimplex

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

English

For any s in stdSimplex S X and any x in X, the value s(x) is nonnegative.

Русский

Для любого s из stdSimplex S X и любого x из X значение s(x) неотрицательно.

LaTeX

$$$\forall s:\,(\mathrm{stdSimplex}\; S\; X).\mathrm{Elem},\forall x:\, X, 0 \le s(x)$$$

Lean4

@[simp]
theorem zero_le (s : stdSimplex S X) (x : X) : 0 ≤ s x :=
  s.2.1 x

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

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

Разделы

Аффилиация

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