restrict_iUnion_ae — Mathlib

English

If a family of sets s_i is pairwise Disjoint, and each s_i is measurable, then restricting to their union distributes over the sum: μ.restrict (⋃ i, s_i) = sum μ.restrict (s_i).

Русский

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

LaTeX

$$$\\mu\\restrict (\\bigcup_i s_i) = \\sum_i (\\mu\\restrict s_i)$, при условиях дискретности и измеримости.$$

Lean4

theorem restrict_iUnion_ae [Countable ι] {s : ι → Set α} (hd : Pairwise (AEDisjoint μ on s))
    (hm : ∀ i, NullMeasurableSet (s i) μ) : μ.restrict (⋃ i, s i) = sum fun i => μ.restrict (s i) :=
  ext fun t ht => by simp only [sum_apply _ ht, restrict_iUnion_apply_ae hd hm ht]

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