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