lintegral_biUnion — Mathlib

English

If t is countable and the s i are measurable with pairwise disjointness, then the lintegral over the biUnion equals the sum over i of the integrals over s_i.

Русский

Если t счётно, а массивы s_i измеримы и попарно несовпадающие, то линеграл по объединению равен сумме интегралов по каждому s_i.

LaTeX

$$$$ \\int^- a in \\bigcup_{i \\in t} s_i, f(a) \\, d\\mu = \\sum_{i \\in t} \\int^- a in s_i, f(a) \\, d\\mu. $$$$

Lean4

theorem lintegral_biUnion {t : Set β} {s : β → Set α} (ht : t.Countable) (hm : ∀ i ∈ t, MeasurableSet (s i))
    (hd : t.PairwiseDisjoint s) (f : α → ℝ≥0∞) : ∫⁻ a in ⋃ i ∈ t, s i, f a ∂μ = ∑' i : t, ∫⁻ a in s i, f a ∂μ :=
  lintegral_biUnion₀ ht (fun i hi => (hm i hi).nullMeasurableSet) hd.aedisjoint f

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