English
Let s be an absorbent subset of a real normed space E, and let r ≥ 0 be such that s is contained in the closed ball of radius r about 0. Then for every x in E, the inequality ∥x∥/r ≤ gauge_s(x) holds.
Русский
Пусть s — абсорбируемое множество в реальном нормированном пространстве E, и пусть r ≥ 0 так, что s ⊆ замкнутый шар радиуса r с центром в 0. Тогда для любого x ∈ E выполняется неравенство ∥x∥/r ≤ gauge_s(x).
LaTeX
$$$\\text{Absorbent}(s) \\wedge 0 \\le r \\wedge s \\subseteq \\overline{B}(0,r) \\;\Rightarrow\; \\frac{\\|x\\|}{r} \\le \\ gauge(s,x).$$$
Lean4
theorem le_gauge_of_subset_closedBall (hs : Absorbent ℝ s) (hr : 0 ≤ r) (hsr : s ⊆ closedBall 0 r) :
‖x‖ / r ≤ gauge s x := by
rw [← gauge_closedBall hr]
exact gauge_mono hs hsr _
