Theorems · Definition · measure theory

MeasurableSpace.GenerateMeasurable.below.casesOn

∀ {α : Type u_1} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.GenerateMeasurable s a → Prop}
  {motive_1 :
    {a : Set α} → (t : MeasurableSpace.GenerateMeasurable s a) → MeasurableSpace.GenerateMeasurable.below t → Prop}
  {a : Set α} {t : MeasurableSpace.GenerateMeasurable s a} (t_1 : MeasurableSpace.GenerateMeasurable.below t),
  (∀ (u : Set α) (a : u ∈ s), motive_1 ⋯ ⋯) →
    motive_1 ⋯ ⋯ →
      (∀ (t : Set α) (a : MeasurableSpace.GenerateMeasurable s t) (ih : MeasurableSpace.GenerateMeasurable.below a)
          (a_ih : motive t a), motive_1 ⋯ ⋯) →
        (∀ (f : ℕ → Set α) (a : ∀ (n : ℕ), MeasurableSpace.GenerateMeasurable s (f n))
            (ih : ∀ (n : ℕ), MeasurableSpace.GenerateMeasurable.below ⋯) (a_ih : ∀ (n : ℕ), motive (f n) ⋯),
            motive_1 ⋯ ⋯) →
          motive_1 t t_1

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Defs

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms