lintegral_biUnion_finset — Mathlib

English

If s is a finite set and t index map to measurable sets, then the lintegral over the union equals the finite sum of the lintegrals over each t b.

Русский

Если s конечен и t(b) измеримы, то линеграл по объединению равен конечной сумме линегралов по t(b).

LaTeX

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

Lean4

theorem lintegral_biUnion_finset {s : Finset β} {t : β → Set α} (hd : Set.PairwiseDisjoint (↑s) t)
    (hm : ∀ b ∈ s, MeasurableSet (t b)) (f : α → ℝ≥0∞) : ∫⁻ a in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ a in t b, f a ∂μ :=
  lintegral_biUnion_finset₀ hd.aedisjoint (fun b hb => (hm b hb).nullMeasurableSet) f

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