Theorems · Theorem · measure theory

aemeasurable_pi_lambda

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {δ : Type u_6} {X : δ → Type u_7}
  {mX : (a : δ) → MeasurableSpace (X a)} [Countable δ] (f : α → (a : δ) → X a),
  (∀ (a : δ), AEMeasurable (fun c => f c a) μ) → AEMeasurable f μ

Defined in

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Cited by

15 results in Mathlib

Foundations

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

Assumes

Countable