Theorems · Theorem · measure theory

Measurable.prod

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {f : α → β × γ}, (Measurable fun a => (f a).1) → (Measurable fun a => (f a).2) → Measurable f

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Constructions

Cited by

9 results in Mathlib

Foundations

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