Theorems · Theorem · measure theory

MeasureTheory.extend_iUnion_le_tsum_nat

∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal},
  m ∅ ⋯ = 0 →
    (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
        Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) →
      ∀ (s : ℕ → Set α), MeasureTheory.extend m (⋃ i, s i) ≤ ∑' (i : ℕ), MeasureTheory.extend m (s i)

Defined in

Mathlib.MeasureTheory.OuterMeasure.Induced

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace