add — Mathlib

English

If f is locally integrable on s, then the function x ↦ ‖f(x)‖ is locally integrable on s.

Русский

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

LaTeX

$$$\\text{LocallyIntegrableOn}(f,s,μ) \\Rightarrow \\text{LocallyIntegrableOn}(\\|f\\|, s, μ)$$$

Lean4

protected theorem add [ContinuousAdd ε''] {f g : X → ε''} (hf : LocallyIntegrableOn f s μ)
    (hg : LocallyIntegrableOn g s μ) : LocallyIntegrableOn (f + g) s μ := fun x hx ↦
  (hf x hx).add
    (hg x hx)
      -- TODO: once mathlib has a ENormedAddCommSubMonoid, generalise this lemma also

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