English
If s is countable, and the family {f b} is pairwise AEDisjoint, and each f b is null-measurable, then μ(⋃ b, f b) = ∑' μ(f b).
Русский
Пусть s счётно, семейство {f b} попарно AEDisjoint и каждое f b нулемеряемо; тогда μ объединения равно сумме мер.
LaTeX
$$$$\\forall s:\\mathrm Set, f:\\, s \\to \\mathrm Set_{\\alpha},\\; s\\text{ Countable} \\rightarrow \\mathrm{Pairwise}(\\mathrm{AEDisjoint}\\,\\mu)\\; f \\;\\Rightarrow\\;\\cdots$$$$
Lean4
theorem measure_biUnion₀ {s : Set β} {f : β → Set α} (hs : s.Countable) (hd : s.Pairwise (AEDisjoint μ on f))
(h : ∀ b ∈ s, NullMeasurableSet (f b) μ) : μ (⋃ b ∈ s, f b) = ∑' p : s, μ (f p) :=
by
haveI := hs.toEncodable
rw [biUnion_eq_iUnion]
exact measure_iUnion₀ (hd.on_injective Subtype.coe_injective fun x => x.2) fun x => h x x.2
