mabs — Mathlib

English

If f tends to a in a topological group, then |f| tends to |a|.

Русский

Если функция сходится к a, то модуль ее значений сходится к модулю a.

LaTeX

$$$\text{Tendsto } f\ l\to (\mathcal{N}\!\!f) \, (\mathcal{N}\!\!a) \Rightarrow \text{ Tendsto } (|f|)\ l\to (|a|).$$$

Lean4

@[to_additive]
protected theorem mabs {a : G} (h : Tendsto f l (𝓝 a)) : Tendsto (fun x => |f x|ₘ) l (𝓝 |a|ₘ) :=
  (continuous_mabs.tendsto _).comp h

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