Theorems · Definition · measure theory

MeasurableSpace.GenerateMeasurable.recOn

∀ {α : Type u_1} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.GenerateMeasurable s a → Prop} {a : Set α}
  (t : MeasurableSpace.GenerateMeasurable s a),
  (∀ (u : Set α) (a : u ∈ s), motive u ⋯) →
    motive ∅ ⋯ →
      (∀ (t : Set α) (a : MeasurableSpace.GenerateMeasurable s t), motive t a → motive tᶜ ⋯) →
        (∀ (f : ℕ → Set α) (a : ∀ (n : ℕ), MeasurableSpace.GenerateMeasurable s (f n)),
            (∀ (n : ℕ), motive (f n) ⋯) → motive (⋃ i, f i) ⋯) →
          motive a t

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Defs

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms