norm — Mathlib

English

If f is locally integrable on s, then the Lp-norm with p = 1 of f is locally integrable on s.

Русский

Если f локально интегрируемо на s, то норма L1 от f локально интегрируема.

LaTeX

$$$\\text{LocallyIntegrableOn}(f,s,μ) \\Rightarrow \\text{LocallyIntegrableOn}(\\|f\\|,s,μ)\\quad (p=1)$$$

Lean4

theorem norm {f : X → E} (hf : LocallyIntegrableOn f s μ) : LocallyIntegrableOn (fun x => ‖f x‖) s μ := fun t ht =>
  let ⟨U, hU_nhd, hU_int⟩ := hf t ht
  ⟨U, hU_nhd, hU_int.norm⟩

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