English
If s is countable, the family f b is pairwise disjoint, and each f b is measurable, then μ(iUnion f b) equals the sum of μ(f b) over b.
Русский
Если s счетно, семейство f b взаимоисключающее, и каждый f b измерим, то мера объединения равна сумме мер.
LaTeX
$$$$\\forall s:\\mathrm Set, f:\\, s \\to \\mathrm Set_{\\alpha},\\; s\\ Countable \\rightarrow \\mathrm{PairwiseDisjoint}\\; f \\;\\rightarrow\\; (\\forall b \\in s, \\mathrm{MeasurableSet}(f(b))) \\rightarrow \\mu(\\bigcup_{b\\in s} f(b)) = \\sum' p:\\, s, \\mu(f(p)).$$$$
Lean4
theorem measure_biUnion {s : Set β} {f : β → Set α} (hs : s.Countable) (hd : s.PairwiseDisjoint f)
(h : ∀ b ∈ s, MeasurableSet (f b)) : μ (⋃ b ∈ s, f b) = ∑' p : s, μ (f p) :=
measure_biUnion₀ hs hd.aedisjoint fun b hb => (h b hb).nullMeasurableSet
