norm — Mathlib

English

If f is IntegrableAtFilter, then the function x ↦ ‖f(x)‖ is IntegrableAtFilter.

Русский

Если f интегрируема на фильтре, то норма ‖f(x)‖ интегрируема.

LaTeX

$$$\\operatorname{IntegrableAtFilter}(f, l, \\mu) \\Rightarrow \\operatorname{IntegrableAtFilter}(\\|f\\|, l, \\mu).$$$

Lean4

protected theorem norm {f : α → E} (hf : IntegrableAtFilter f l μ) : IntegrableAtFilter (fun x => ‖f x‖) l μ :=
  Exists.casesOn hf fun s hs ↦ ⟨s, hs.1, hs.2.norm⟩

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