English
For a countable family of sets S, pairwise AEDisjoint, and each S element null-measurable, μ(⋃₀ S) equals the sum over S of μ.
Русский
Для счетного множества множеств S, попарно AEDisjoint, и каждого элемента S нулемеряемо, μ(union S) равно сумме μ.
LaTeX
$$$$\\forall S:\\mathrm Set (\\mathrm Set α),\\; S.Countable \\rightarrow S.Pairwise (\\mathrm AEDisjoint\\, \\mu) \\rightarrow (\\forall s \\in S, \\mathrm NullMeasurableSet s \\mu) \\rightarrow \\mu(\\bigcup_{s\\in S} s) = \\sum' s:\\, S, \\mu(s).$$$$
Lean4
theorem measure_sUnion₀ {S : Set (Set α)} (hs : S.Countable) (hd : S.Pairwise (AEDisjoint μ))
(h : ∀ s ∈ S, NullMeasurableSet s μ) : μ (⋃₀ S) = ∑' s : S, μ s := by
rw [sUnion_eq_biUnion, measure_biUnion₀ hs hd h]