English
Let s be a convex subset of a topological vector space, and assume that 0 belongs to its nhd neighborhood. Then the gauge of s at x is at most 1 if and only if x lies in the closure of s.
Русский
Пусть s — выпуклоe множество в топологическом векторном пространстве, и 0 принадлежит окрестности s. Тогда gauge(s, x) ≤ 1 тогда и только тогда, когда x принадлежит замыканию s.
LaTeX
$$$\\operatorname{gauge}(s,x) \\le 1 \\iff x \\in \\overline{s}$$$
Lean4
theorem gauge_le_one_iff_mem_closure (hc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) : gauge s x ≤ 1 ↔ x ∈ closure s :=
⟨mem_closure_of_gauge_le_one hc (mem_of_mem_nhds hs₀) (absorbent_nhds_zero hs₀), fun h ↦
le_on_closure (fun _ ↦ gauge_le_one_of_mem) (continuous_gauge hc hs₀).continuousOn continuousOn_const h⟩
