Theorems · Theorem · measure theory

MeasureTheory.Measure.prod_def

∀ {α : Type u_4} {β : Type u_5} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure β), μ.prod ν = μ.bind fun x => MeasureTheory.Measure.map (Prod.mk x) ν

Defined in

Mathlib.MeasureTheory.Measure.Prod

Cited by

6 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace