lintegral_iUnion — Mathlib

English

If each s_i is measurable and the s_i are pairwise disjoint, then the lintegral over the union is the sum of the lintegrals over each s_i.

Русский

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

LaTeX

$$$$ \\int^- a \\in \\bigcup_i s_i, f(a) \\, d\\mu = \\sum_i \\int^- a \\in s_i, f(a) \\, d\\mu. $$$$

Lean4

theorem lintegral_iUnion [Countable β] {s : β → Set α} (hm : ∀ i, MeasurableSet (s i)) (hd : Pairwise (Disjoint on s))
    (f : α → ℝ≥0∞) : ∫⁻ a in ⋃ i, s i, f a ∂μ = ∑' i, ∫⁻ a in s i, f a ∂μ :=
  lintegral_iUnion₀ (fun i => (hm i).nullMeasurableSet) hd.aedisjoint f

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