countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top

English

In an s-finite space, among disjoint null-measurable sets, the subset with positive measure is countable.

Русский

В s-конечной пространстве, среди попарно непересекающихся нулево-мерассматриваемых множеств, множество с положительной мерой счётно.

LaTeX

$$In a finite space, {i : μ(A_i) > 0} is countable$$

Lean4

/-- If the union of disjoint 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 : ι, MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As))
    (Union_As_finite : μ (⋃ i, As i) ≠ ∞) : Set.Countable {i : ι | 0 < μ (As i)} :=
  countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ μ (fun i ↦ (As_mble i).nullMeasurableSet)
    ((fun _ _ h ↦ Disjoint.aedisjoint (As_disj h))) Union_As_finite

Похожие утверждения