tendsto_norm' — Mathlib

English

The map a ↦ ‖a‖ is continuous at every point x in a seminormed group E; in particular, at x it tends to ‖x‖ as a → x.

Русский

Отображение a ↦ ‖a‖ непрерывно в любой точке x в полугруппе с нормой; в частности, при a → x стремится к ‖x‖.

LaTeX

$$$ \operatorname{Tendsto}\left( a \mapsto \|a\| \right)\left( \mathcal{N}(x) \right)\left( \mathcal{N}(\|x\|) \right). $$$$

Lean4

@[to_additive tendsto_norm]
theorem tendsto_norm' {x : E} : Tendsto (fun a => ‖a‖) (𝓝 x) (𝓝 ‖x‖) := by
  simpa using tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (1 : E)) _ _)

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