English
For a family As : ι → Set α with As_mble: ∀ i, NullMeasurableSet (As i) μ and As_disj: Pairwise (AEDisjoint μ on As), we have (∑' i, μ(As i)) ≤ μ(⋃ i, As i).
Русский
Пусть семейство As: ι → Set α таково, что каждый As(i) нулемеримо измеримо и As сортируется как пара-дездер, тогда сумма мер по As не превосходит меру объединения.
LaTeX
$$$$ \\sum\\nabla i, \\mu(As_i) \\le \\mu\\left(\\bigcup_{i} As_i\\right). $$$$
Lean4
/-- The measure of an a.e. disjoint union (even uncountable) of null-measurable sets is at least
the sum of the measures of the sets. -/
theorem tsum_meas_le_meas_iUnion_of_disjoint₀ {ι : Type*} {_ : MeasurableSpace α} (μ : Measure α) {As : ι → Set α}
(As_mble : ∀ i : ι, NullMeasurableSet (As i) μ) (As_disj : Pairwise (AEDisjoint μ on As)) :
(∑' i, μ (As i)) ≤ μ (⋃ i, As i) :=
by
rw [ENNReal.tsum_eq_iSup_sum, iSup_le_iff]
intro s
simp only [← measure_biUnion_finset₀ (fun _i _hi _j _hj hij => As_disj hij) fun i _ => As_mble i]
gcongr
exact iUnion_subset fun _ ↦ Subset.rfl
