Theorems · Theorem · measure theory

MeasurableSpace.generateFrom_induction

∀ {α : Type u_1} (C : Set (Set α)) (p : (s : Set α) → MeasurableSet s → Prop),
  (∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht) →
    p ∅ ⋯ →
      (∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯) →
        (∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯) →
          ∀ (s : Set α) (hs : MeasurableSet s), p s hs

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Defs

Cited by

7 results in Mathlib

Foundations

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