lintegral_add_left' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lintegral_add_left' {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (g : α → ℝ≥0∞) :
    ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ := by
  rw [lintegral_congr_ae hf.ae_eq_mk, ← lintegral_add_left hf.measurable_mk,
    lintegral_congr_ae (hf.ae_eq_mk.fun_add (ae_eq_refl g))]

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