English
Let s be a finite index set and f: s → Set α. If the family {f(b)} is almost disjoint with respect to μ and each f(b) is null-measurable, then μ(⋃ b ∈ s, f(b)) = ∑ p ∈ s μ(f(p)).
Русский
Пусть s — конечное множество индексов и f: s → множество α. Если семейство {f(b)} попарно μ-практически непересекается и каждый f(b) нулемеримо измеримо, то μ(⋃_{b∈s} f(b)) = ∑_{p∈s} μ(f(p)).
LaTeX
$$$$ \\mu\\left(\\bigcup_{b \\in s} f(b)\\right) = \\sum_{p \\in s} \\mu\\left(f(p)\\right). $$$$
Lean4
theorem measure_biUnion_finset₀ {s : Finset ι} {f : ι → Set α} (hd : Set.Pairwise (↑s) (AEDisjoint μ on f))
(hm : ∀ b ∈ s, NullMeasurableSet (f b) μ) : μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p) :=
by
rw [← Finset.sum_attach, Finset.attach_eq_univ, ← tsum_fintype (L := .unconditional s)]
exact measure_biUnion₀ s.countable_toSet hd hm
