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 (f + g) μ :=
  ⟨hf.aestronglyMeasurable.add hg.aestronglyMeasurable, hf.add' hg⟩

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