English
The gauge is always nonnegative for any x.
Русский
Gauge всегда неотрицательна для любого x.
LaTeX
$$$$ 0 \\le \\operatorname{gauge}(s, x). $$$$
Lean4
/-- The gauge evaluated at `0` is always zero (mathematically this requires `0` to be in the set `s`
but, the real infimum of the empty set in Lean being defined as `0`, it holds unconditionally). -/
@[simp]
theorem gauge_zero : gauge s 0 = 0 := by
rw [gauge_def']
by_cases h : (0 : E) ∈ s
· simp only [smul_zero, sep_true, h, csInf_Ioi]
· simp only [smul_zero, sep_false, h, Real.sInf_empty]