English
In an s-finite space, among disjoint null-measurable sets, only countably many can have positive measure.
Русский
В s-конечном пространстве, среди попарно непересекающихся нулево-мерассматриваемых множеств, только счётное число имеет положительную меру.
LaTeX
$$countable {i : ι | 0 < μ(As i)}$$
Lean4
/-- In an s-finite space, among disjoint null-measurable sets, only countably many can have positive
measure. -/
theorem countable_meas_pos_of_disjoint_iUnion₀ {ι : Type*} {_ : MeasurableSpace α} {μ : Measure α} [SFinite μ]
{As : ι → Set α} (As_mble : ∀ i : ι, NullMeasurableSet (As i) μ) (As_disj : Pairwise (AEDisjoint μ on As)) :
Set.Countable {i : ι | 0 < μ (As i)} :=
by
rw [← sum_sfiniteSeq μ] at As_disj As_mble ⊢
have obs : {i : ι | 0 < sum (sfiniteSeq μ) (As i)} ⊆ ⋃ n, {i : ι | 0 < sfiniteSeq μ n (As i)} :=
by
intro i hi
by_contra con
simp only [mem_iUnion, mem_setOf_eq, not_exists, not_lt, nonpos_iff_eq_zero] at *
rw [sum_apply₀] at hi
· simp_rw [con] at hi
simp at hi
· exact As_mble i
apply Countable.mono obs
refine countable_iUnion fun n ↦ ?_
apply countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀
· exact fun i ↦ (As_mble i).mono (le_sum _ _)
· exact fun i j hij ↦ AEDisjoint.of_le (As_disj hij) (le_sum _ _)
· exact measure_ne_top _ (⋃ i, As i)
