gauge_nonneg

Mathlib.Analysis.Convex.Gauge

URI: https://scilib.ai/kg/mathlib#gauge_nonneg

English

For every x, gauge(s,x) is nonnegative.

Русский

Для каждого x gauge(s,x) неотрицательно.

LaTeX

$$$$ 0 \\le \\operatorname{gauge}(s, x). $$$$

Lean4

/-- The gauge is always nonnegative. -/
theorem gauge_nonneg (x : E) : 0 ≤ gauge s x :=
  Real.sInf_nonneg fun _ hx => hx.1.le

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

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

Разделы

Аффилиация

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