continuous_gauge — Mathlib

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₀

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