Theorems · Theorem · measure theory

MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum

∀ {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent ENNReal C},
  MeasureTheory.IsSetRing C →
    (∀ (f : ℕ → Set α),
        (∀ (i : ℕ), f i ∈ C) →
          ⋃ i, f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)) →
      ∀ ⦃f : ℕ → Set α⦄,
        Monotone f →
          (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Filter.Tendsto (fun n => m (f n)) Filter.atTop (nhds (m (⋃ i, f i)))

If an additive content is σ-additive on a set ring, then the content of a monotone sequence of sets tends to the content of the union.

Defined in

Mathlib.MeasureTheory.Measure.AddContent

Cited by

1 results in Mathlib

Foundations

Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound