English
If s is convex, 0 ∈ s, and s is absorbent, then the sublevel {x | gauge s x ≤ a} is convex for a ≥ 0; for a < 0 it is empty.
Русский
Если s выпукло, 0∈s и поглощающее, то подмножество {x: gauge s x ≤ a} выпукло при a ≥ 0; если a < 0, оно пустое.
LaTeX
$$$$(\\text{Convex}(s)) \\land (0 \\in s) \\land (\\text{Absorbent}(s)) \\Rightarrow \\\\text{Convex}\\{x : \\mathrm{gauge}(s,x) \\le a\\} \\text{ for } a \\ge 0, \\text{ and empty if } a < 0.$$$$
Lean4
theorem gauge_le (hs : Convex ℝ s) (h₀ : (0 : E) ∈ s) (absorbs : Absorbent ℝ s) (a : ℝ) :
Convex ℝ {x | gauge s x ≤ a} := by
by_cases ha : 0 ≤ a
· rw [gauge_le_eq hs h₀ absorbs ha]
exact convex_iInter fun i => convex_iInter fun _ => hs.smul _
· convert convex_empty (𝕜 := ℝ)
exact eq_empty_iff_forall_notMem.2 fun x hx => ha <| (gauge_nonneg _).trans hx
