lintegral_add_right' — Mathlib

English

Let f,g: α → ℝ≥0∞ with g being AEMeasurable. Then ∫⁻ (f+g) = ∫⁻ f + ∫⁻ g.

Русский

Пусть f,g: α → ℝ≥0∞ и g является AEMeasurable. Тогда ∫⁻ (f+g) = ∫⁻ f + ∫⁻ g.

LaTeX

$$$\forall f : α \to \mathbb{R}_{\ge 0}^{\infty},\; {g : α \to \mathbb{R}_{\ge 0}^{\infty}}\; (hg : \mathrm{AEMeasurable}\, g\, \mu) \Rightarrow ∫^- a, f a + g a \partial\mu = ∫^- a, f a \partial\mu + ∫^- a, g a \partial\mu$$$

Lean4

theorem lintegral_add_right' (f : α → ℝ≥0∞) {g : α → ℝ≥0∞} (hg : AEMeasurable g μ) :
    ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ := by simpa only [add_comm] using lintegral_add_left' hg f

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