English
Under pairwise disjointness and null measurability of the sets, the union measure equals the sum of measures.
Русский
При попарном несовпадении и нулевой измеримости множества равенство меры объединения и суммы мер.
LaTeX
$$$\\forall \\text{Countable } ι, \\ {f : ι → Set α}, \\ (\\text{Pairwise } (AEDisjoint μ on f)) \\, (\\forall i, NullMeasurableSet (f i) μ) \\Rightarrow μ(⋃ i, f i) = ∑' i, μ(f i)$$$
Lean4
theorem measure_iUnion₀ [Countable ι] {f : ι → Set α} (hd : Pairwise (AEDisjoint μ on f))
(h : ∀ i, NullMeasurableSet (f i) μ) : μ (⋃ i, f i) = ∑' i, μ (f i) :=
by
rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, _ht_sub, ht_eq, htm, htd⟩
calc
μ (⋃ i, f i) = μ (⋃ i, t i) := measure_congr (EventuallyEq.countable_iUnion ht_eq)
_ = ∑' i, μ (t i) := (measure_iUnion htd htm)
_ = ∑' i, μ (f i) := tsum_congr fun i => measure_congr (ht_eq _).symm
