Theorems · Theorem · measure theory

Measurable.prodMk

∀ {α : Type u_1} {m : MeasurableSpace α} {β : Type u_6} {γ : Type u_7} {x : MeasurableSpace β} {x_1 : MeasurableSpace γ}
  {f : α → β} {g : α → γ}, Measurable f → Measurable g → Measurable fun a => (f a, g a)

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Constructions

Cited by

115 results in Mathlib

Foundations

Depth 71 from the axioms, rests on 750 definitions · uses propext, Classical.choice, Quot.sound