egauge_le_of_mem_smul

Mathlib.Analysis.Convex.EGauge

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

English

If x ∈ c · s, then egauge_s(x) ≤ ∥c∥_e.

Русский

Если x ∈ c · s, то egauge_s(x) ≤ ∥c∥_e.

LaTeX

$$$x \in c \cdot s \Rightarrow \mathrm{egauge}_{\mathbb{K}}(s,x) \le \|c\|_e$$$

Lean4

theorem egauge_le_of_mem_smul (h : x ∈ c • s) : egauge 𝕜 s x ≤ ‖c‖ₑ :=
  iInf₂_le c h

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

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

Разделы

Аффилиация

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