English
If s is convex, 0 ∈ s, and s is absorbent, then {x : gauge s x < 1} ⊆ s.
Русский
Пусть s выпукло, 0 ∈ s и s поглощающее. Тогда {x : gauge s x < 1} ⊆ s.
LaTeX
$$$$(\\operatorname{Convex}_{\\mathbb{R}}(s)) \\land (0 \\in s) \\land (\\operatorname{Absorbent}_{\\mathbb{R}}(s)) \\Rightarrow \\{x \\in E \\mid \\mathrm{gauge}(s,x) < 1\\} \\subseteq s.$$$$
Lean4
theorem gauge_lt_one_subset_self (hs : Convex ℝ s) (h₀ : (0 : E) ∈ s) (absorbs : Absorbent ℝ s) :
{x | gauge s x < 1} ⊆ s := fun _x hx ↦
let ⟨_y, hys, hx⟩ := mem_openSegment_of_gauge_lt_one absorbs hx
hs.openSegment_subset h₀ hys hx