English
If the union of a family of pairwise disjoint null-measurable sets has finite measure, then only finitely many of them have measure at least ε > 0.
Русский
Если объединение попарно непересекающихся нуль-мерарассматриваемых множеств имеет конечную меру, то лишь конечное число из них имеют меру не менее ε > 0.
LaTeX
$$Under given conditions, {i : ε ≤ μ(As i)} is finite$$
Lean4
/-- If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only
countably many members of the union whose measure is positive. -/
theorem countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ {ι : Type*} {_ : MeasurableSpace α} (μ : Measure α)
{As : ι → Set α} (As_mble : ∀ i : ι, NullMeasurableSet (As i) μ) (As_disj : Pairwise (AEDisjoint μ on As))
(Union_As_finite : μ (⋃ i, As i) ≠ ∞) : Set.Countable {i : ι | 0 < μ (As i)} :=
by
set posmeas := {i : ι | 0 < μ (As i)} with posmeas_def
rcases exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ≥0∞) < 1) with ⟨as, _, as_mem, as_lim⟩
set fairmeas := fun n : ℕ => {i : ι | as n ≤ μ (As i)}
have countable_union : posmeas = ⋃ n, fairmeas n :=
by
have fairmeas_eq : ∀ n, fairmeas n = (fun i => μ (As i)) ⁻¹' Ici (as n) := fun n =>
by
simp only [fairmeas]
rfl
simpa only [fairmeas_eq, posmeas_def, ← preimage_iUnion,
iUnion_Ici_eq_Ioi_of_lt_of_tendsto (fun n => (as_mem n).1) as_lim]
rw [countable_union]
refine countable_iUnion fun n => Finite.countable ?_
exact finite_const_le_meas_of_disjoint_iUnion₀ μ (as_mem n).1 As_mble As_disj Union_As_finite
