Theorems · Theorem · measure theory

Measurable.eval

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

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Constructions

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace