English
The gauge of the closure of {0} is the zero function; equivalently, gauge(closure({0})) = 0.
Русский
Gauge замыкания множества {0} равно нулю.
LaTeX
$$$\\operatorname{gauge}(\\operatorname{closure}({0})) = 0$$$
Lean4
@[simp]
theorem gauge_closure_zero : gauge (closure (0 : Set E)) = 0 :=
funext fun x ↦
by
simp only [← singleton_zero, gauge_def', mem_closure_zero_iff_norm, norm_smul, mul_eq_zero, norm_eq_zero,
inv_eq_zero]
rcases (norm_nonneg x).eq_or_lt' with hx | hx
· convert csInf_Ioi (a := (0 : ℝ))
exact Set.ext fun r ↦ and_iff_left (.inr hx)
· convert Real.sInf_empty
exact eq_empty_of_forall_notMem fun r ⟨hr₀, hr⟩ ↦ hx.ne' <| hr.resolve_left hr₀.out.ne'
