English
If s is absorbent, then for any a ∈ ℝ, the set {x : gauge s x < a} equals the union over all r > 0 with r < a of r · s.
Русский
Пусть s — поглощающее множество. Тогда для любого a ∈ ℝ множество {x : gauge s x < a} равно объединению по всем r > 0 и r < a множества r · s.
LaTeX
$$$$(\\operatorname{Absorbent}_{\\mathbb{R}}(s)) \\Rightarrow \\{x \\in E \\mid \\mathrm{gauge}(s,x) < a\\} = \\bigcup_{r > 0,\\; r < a} r\\,s.$$$$
Lean4
theorem gauge_lt_eq' (absorbs : Absorbent ℝ s) (a : ℝ) :
{x | gauge s x < a} = ⋃ (r : ℝ) (_ : 0 < r) (_ : r < a), r • s :=
by
ext
simp_rw [mem_setOf, mem_iUnion, exists_prop]
exact ⟨exists_lt_of_gauge_lt absorbs, fun ⟨r, hr₀, hr₁, hx⟩ => (gauge_le_of_mem hr₀.le hx).trans_lt hr₁⟩
