English
If s is a convex neighborhood of the origin and s is near zero, then the gauge function gauge s is continuous.
Русский
Если s выпуклый окрестности начала и близко к нулю, то функция gauge s непрерывна.
LaTeX
$$$Continuous (gauge s)$$$
Lean4
/-- If `s` is a convex neighborhood of the origin in a topological real vector space, then `gauge s`
is continuous. If the ambient space is a normed space, then `gauge s` is Lipschitz continuous, see
`Convex.lipschitz_gauge`. -/
@[continuity, fun_prop]
theorem continuous_gauge (hc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) : Continuous (gauge s) :=
continuous_iff_continuousAt.2 fun _ ↦ continuousAt_gauge hc hs₀