Theorems · Theorem · measure theory

MeasurableSpace.GenerateMeasurable.brecOn

∀ {α : Type u_1} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.GenerateMeasurable s a → Prop} {a : Set α}
  (t : MeasurableSpace.GenerateMeasurable s a),
  (∀ (a : Set α) (t : MeasurableSpace.GenerateMeasurable s a),
      MeasurableSpace.GenerateMeasurable.below t → motive a t) →
    motive a t

Defined in: Mathlib.MeasureTheory.MeasurableSpace.Defs
Cited by: 0 results in Mathlib
Foundations: Depth 8 from the axioms · uses no axioms

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
MeasurableSpace.GenerateMeasurablestatement and proof · cited by 11
MeasurableSpace.GenerateMeasurable.belowstatement and proof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.