add'' — Mathlib

English

If f is integrable, then f + g is integrable iff g is integrable.

Русский

Если f интегрируемо, то f + g интегрируемо тогда и только тогда, когда g интегрируемо.

LaTeX

$$$\\mathrm{Integrable}(f, μ) \\Rightarrow (\\mathrm{Integrable}(f+g, μ) \\iff \\mathrm{Integrable}(g, μ)).$$$

Lean4

@[fun_prop]
theorem add'' [ContinuousAdd ε'] {f g : α → ε'} (hf : Integrable f μ) (hg : Integrable g μ) :
    Integrable (fun x ↦ f x + g x) μ :=
  hf.add hg

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