English
If s is convex and the origin is in the interior of s (in the nhds sense), then gauge s is Lipschitz on some neighborhood of the origin; in particular, gauge s is globally Lipschitz on the space if nhds(0) ⊆ s.
Русский
Если s выпуклоe и нуль лежит во внутренности s в топологии, то gauge s липшицев в некоторой окрестности нуля; в частности, gauge может быть глобально липшицевым при условии nhds(0) ⊆ s.
LaTeX
$$$$ \exists K>0\; \text{ such that }\mathrm{LipschitzWith}(K)\bigl(\mathrm{gauge}(s)\bigr). $$$$
Lean4
theorem lipschitz_gauge (hc : Convex ℝ s) (h₀ : s ∈ 𝓝 (0 : E)) : ∃ K, LipschitzWith K (gauge s) :=
let ⟨r, hr₀, hr⟩ := Metric.mem_nhds_iff.1 h₀
⟨(⟨r, hr₀.le⟩ : ℝ≥0)⁻¹, hc.lipschitzWith_gauge hr₀ hr⟩
