gauge_zero' — Mathlib

English

Gauge on the empty set is zero; gauge on the singleton {0} is zero.

Русский

Gauge на пустом множестве равна нулю; gauge на множестве {0} равна нулю.

LaTeX

$$$$\\operatorname{gauge}(\\emptyset) = 0, \\quad \\operatorname{gauge}(\\{0\\}) = 0.$$$$

Lean4

@[simp]
theorem gauge_zero' : gauge (0 : Set E) = 0 := by
  ext x
  rw [gauge_def']
  obtain rfl | hx := eq_or_ne x 0
  · simp only [csInf_Ioi, mem_zero, Pi.zero_apply, sep_true, smul_zero]
  · simp only [mem_zero, Pi.zero_apply, inv_eq_zero, smul_eq_zero]
    convert Real.sInf_empty
    exact eq_empty_iff_forall_notMem.2 fun r hr => hr.2.elim (ne_of_gt hr.1) hx

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