mem_of_egauge_lt_one

Mathlib.Analysis.Convex.EGauge

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

English

If Balanced s and egauge s x < 1, then x ∈ s.

Русский

Если Balanced s и egauge s x < 1, тогда x ∈ s.

LaTeX

$$$\text{Balanced } s \land \mathrm{egauge}_{\mathbb{K}}(s,x) < 1 \Rightarrow x \in s$$$

Lean4

theorem mem_of_egauge_lt_one (hs : Balanced 𝕜 s) (hx : egauge 𝕜 s x < 1) : x ∈ s :=
  one_smul 𝕜 s ▸ mem_smul_of_egauge_lt hs (by simpa)

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

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

Разделы

Аффилиация

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