countable_meas_pos_of_disjoint_iUnion

English

In an s-finite space, among disjoint measurable sets, only countably many can have positive measure.

Русский

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

LaTeX

$$countable {i : ι | 0 < μ(A_i)}$$

Lean4

/-- In an s-finite space, among disjoint 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 : ι, MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As)) :
    Set.Countable {i : ι | 0 < μ (As i)} :=
  countable_meas_pos_of_disjoint_iUnion₀ (fun i ↦ (As_mble i).nullMeasurableSet)
    ((fun _ _ h ↦ Disjoint.aedisjoint (As_disj h)))

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