Theorems · Theorem · measure theory

measurable_from_prod_countable_right

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  [Countable α] [MeasurableSingletonClass α] {f : α × β → γ}, (∀ (x : α), Measurable fun y => f (x, y)) → Measurable f

For the version where the second space in the product is countable, see measurable_from_prod_countable_left.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Constructions

Cited by

0 results in Mathlib

Foundations

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

Assumes

CountableMeasurableSingletonClass