lintegral_iUnion₀ — Mathlib

English

For a countable index set and a family of null-measurable sets, the lintegral over the union equals the sum of the individual lintegrals.

Русский

Для счётного множителя и семейства нуль-при-meасируемых множеств интеграл по объединению равен сумме интегралов по каждому множеству.

LaTeX

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

Lean4

theorem lintegral_iUnion₀ [Countable β] {s : β → Set α} (hm : ∀ i, NullMeasurableSet (s i) μ)
    (hd : Pairwise (AEDisjoint μ on s)) (f : α → ℝ≥0∞) : ∫⁻ a in ⋃ i, s i, f a ∂μ = ∑' i, ∫⁻ a in s i, f a ∂μ := by
  simp only [Measure.restrict_iUnion_ae hd hm, lintegral_sum_measure]

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