gauge_zero — Mathlib

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]

Похожие утверждения