integral_union_ae — Mathlib

English

For disjoint measurable sets s and t, the integral over their union equals the sum of integrals over each set.

Русский

Для непересекающихся измеримых множеств s и t интеграл по их объединению равен сумме интегралов по каждому множеству.

LaTeX

$$$\\int_{x \\in s \\cup t} f(x) \\,d\\mu = \\int_{x \\in s} f(x) \\,d\\mu + \\int_{x \\in t} f(x) \\,d\\mu$$$

Lean4

theorem integral_union_ae (hst : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) (hfs : IntegrableOn f s μ)
    (hft : IntegrableOn f t μ) : ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ + ∫ x in t, f x ∂μ := by
  simp only [Measure.restrict_union₀ hst ht, integral_add_measure hfs hft]

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