Theorems · Theorem · measure theory

aemeasurable_pi_iff

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

Defined in

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Cited by

3 results in Mathlib

Foundations

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

Assumes

Countable