integral_iUnion — Mathlib

English

For countable family of sets s_i with disjointness, the integral over the union equals the sum of integrals over each s_i.

Русский

Для счётной семейства множеств s_i с распадом на непересекающиеся части интеграл по объединению равен сумме интегралов по каждому s_i.

LaTeX

$$$$ \int_{x \in \bigcup_{n} s_n} f(x) \, d\mu = \sum_{n} \int_{x \in s_n} f(x) \, d\mu $$$$

Lean4

theorem integral_iUnion {ι : Type*} [Countable ι] {s : ι → Set X} (hm : ∀ i, MeasurableSet (s i))
    (hd : Pairwise (Disjoint on s)) (hfi : IntegrableOn f (⋃ i, s i) μ) :
    ∫ x in ⋃ n, s n, f x ∂μ = ∑' n, ∫ x in s n, f x ∂μ :=
  (HasSum.tsum_eq (hasSum_integral_iUnion hm hd hfi)).symm

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