English
For a countable index set, the measure of a union equals the sum of measures when the sets are pairwise disjoint and measurable.
Русский
Для счётного множества индексов мера объединения равна сумме мер, если множества попарно не пересекаются и измеримы.
LaTeX
$$$\\forall ι\\, [Countable ι], \\ \\forall f : ι → Set α,\\ (\\text{Pairwise } (Disjoint on f)) \\to (\\forall i, MeasurableSet (f i)) \\Rightarrow μ(\\bigcup_i f(i)) = \\sum' i, μ(f(i))$$$
Lean4
theorem measure_iUnion {m0 : MeasurableSpace α} {μ : Measure α} [Countable ι] {f : ι → Set α}
(hn : Pairwise (Disjoint on f)) (h : ∀ i, MeasurableSet (f i)) : μ (⋃ i, f i) = ∑' i, μ (f i) :=
by
rw [measure_eq_extend (MeasurableSet.iUnion h), extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]
· simp [measure_eq_extend, h]
· exact μ.empty
· exact μ.m_iUnion
