self_subset_gauge_le_one

Mathlib.Analysis.Convex.Gauge

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

English

If s is convex, then s ⊆ {x : gauge s x ≤ 1}. Equivalently, the unit gauge ball contains s.

Русский

Если s выпукло, то s ⊆ {x : gauge s x ≤ 1}. Иными словами, единичная штанга по gauge содержит s.

LaTeX

$$$$s \\subseteq \\{x \\mid \\mathrm{gauge}(s,x) \\le 1\\}.$$$$

Lean4

theorem self_subset_gauge_le_one : s ⊆ {x | gauge s x ≤ 1} := fun _ => gauge_le_one_of_mem

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

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

Разделы

Аффилиация

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