continuousAt_gauge_zero — Mathlib

English

If s is a convex neighborhood of the origin, gauge s is continuous at the origin.

Русский

Если s - выпуклая окрестность нуля, gauge s непрерывна в нуле.

LaTeX

$$$$ \\operatorname{ContinuousAt}(\\operatorname{gauge}(s),0). $$$$

Lean4

/-- If `s` is a neighborhood of the origin, then `gauge s` is continuous at the origin.
See also `continuousAt_gauge`. -/
theorem continuousAt_gauge_zero (hs : s ∈ 𝓝 0) : ContinuousAt (gauge s) 0 :=
  by
  rw [ContinuousAt, gauge_zero]
  exact tendsto_gauge_nhds_zero hs

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