nnnorm' — Mathlib

English

If f tends to a, then the nnnorm of f also tends to the nnnorm of the limit, i.e., Tendsto of ‖f x‖₊ to ‖a‖₊.

Русский

Если f сходится к a, то сходится и ‖f‖₊ к ‖a‖₊.

LaTeX

$$$ \operatorname{Tendsto}\left( f \right) \to (\mathcal{N}) $$$

Lean4

@[to_additive Filter.Tendsto.nnnorm]
theorem nnnorm' (h : Tendsto f l (𝓝 a)) : Tendsto (fun x => ‖f x‖₊) l (𝓝 ‖a‖₊) :=
  Tendsto.comp continuous_nnnorm'.continuousAt h

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