gauge_def

Mathlib.Analysis.Convex.Gauge

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

English

The same gauge can be defined by using x in r^{-1} s or equivalently by a different infimum description.

Русский

Та же gauge может быть определена через x∈ r^{-1} s, эквивалентно другой формулировке инфима.

LaTeX

$$$$\\operatorname{gauge}(s,x) = \\inf\\{ r>0 : r^{-1} \\cdot x \\in s \\}.$$$$

Lean4

theorem gauge_def : gauge s x = sInf ({r ∈ Set.Ioi (0 : ℝ) | x ∈ r • s}) :=
  rfl

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

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

Разделы

Аффилиация

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