English
Let f: α → ℝ≥0∞ and g: α → ℝ≥0∞ with g measurable. Then ∫⁻ (f+g) = ∫⁻ f + ∫⁻ g.
Русский
Пусть f: α → ℝ≥0∞ и g: α → ℝ≥0∞; если g измерима, то ∫⁻ (f+g) dμ = ∫⁻ f dμ + ∫⁻ g dμ.
LaTeX
$$$\forall f : α \to \mathbb{R}_{\ge 0}^{\infty},\; {g : α \to \mathbb{R}_{\ge 0}^{\infty}}\; (hg : \mathrm{Measurable}\, g) \Rightarrow ∫^- a, f a + g a \partial\mu = ∫^- a, f a \partial\mu + ∫^- a, g a \partial\mu$$$
Lean4
/-- If `f g : α → ℝ≥0∞` are two functions and one of them is (a.e.) measurable, then the Lebesgue
integral of `f + g` equals the sum of integrals. This lemma assumes that `g` is integrable, see also
`MeasureTheory.lintegral_add_left` and primed versions of these lemmas. -/
@[simp]
theorem lintegral_add_right (f : α → ℝ≥0∞) {g : α → ℝ≥0∞} (hg : Measurable g) :
∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ :=
lintegral_add_right' f hg.aemeasurable
