Theorems · Theorem · measure theory

MeasureTheory.inducedOuterMeasure_caratheodory

∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
  (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
    (∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
      ∀ (s : Set α),
        MeasurableSet s ↔
          ∀ (t : Set α),
            P t →
              (MeasureTheory.inducedOuterMeasure m P0 m0) (t ∩ s) +
                  (MeasureTheory.inducedOuterMeasure m P0 m0) (t \ s) ≤
                (MeasureTheory.inducedOuterMeasure m P0 m0) t

To test whether s is Carathéodory-measurable we only need to check the sets t for which P t holds. See ofFunction_caratheodory for another way to show the Carathéodory-measurability of s.

Defined in

Mathlib.MeasureTheory.OuterMeasure.Induced

Cited by

1 results in Mathlib

Foundations

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