Theorems · Theorem · measure theory

measurable_pi_iff

∀ {α : Type u_1} {δ : Type u_4} {X : δ → Type u_6} [inst : MeasurableSpace α] [inst_1 : (a : δ) → MeasurableSpace (X a)]
  {g : α → (a : δ) → X a}, Measurable g ↔ ∀ (a : δ), Measurable fun x => g x a

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Constructions

Cited by

21 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace