English
Under the same assumptions, gauge s x = 0 iff x = 0 (alternative formulation).
Русский
При тех же предположениях gauge s x = 0 тогда и только тогда x = 0 (альтернативная формулировка).
LaTeX
$$$$\\mathrm{gauge}(s,x) = 0 \\iff x = 0.$$$$
Lean4
theorem gauge_eq_zero (hs : Absorbent ℝ s) (hb : Bornology.IsVonNBounded ℝ s) : gauge s x = 0 ↔ x = 0 :=
by
refine ⟨fun h₀ ↦ by_contra fun (hne : x ≠ 0) ↦ ?_, fun h ↦ h.symm ▸ gauge_zero⟩
have : { x }ᶜ ∈ comap (gauge s) (𝓝 0) := comap_gauge_nhds_zero_le hs hb (isOpen_compl_singleton.mem_nhds hne.symm)
rcases ((nhds_basis_zero_abs_lt _).comap _).mem_iff.1 this with ⟨r, hr₀, hr⟩
exact hr (by simpa [h₀]) rfl
