Theorems · Theorem · measure theory

MeasurableSet.induction_on_open

∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [inst_2 : BorelSpace γ]
  {C : (s : Set γ) → MeasurableSet s → Prop},
  (∀ (U : Set γ) (hU : IsOpen U), C U ⋯) →
    (∀ (t : Set γ) (ht : MeasurableSet t), C t ht → C tᶜ ⋯) →
      (∀ (f : ℕ → Set γ),
          Pairwise (Function.onFun Disjoint f) →
            ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯) →
        ∀ (t : Set γ) (ht : MeasurableSet t), C t ht

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpace