Theorems · Theorem · measure theory

MeasureTheory.ProbabilityMeasure.map_prod_map

∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) {α' : Type u_3}
  [inst_2 : MeasurableSpace α'] {β' : Type u_4} [inst_3 : MeasurableSpace β'] {f : α → α'} {g : β → β'}
  (f_mble : Measurable f) (g_mble : Measurable g), (μ.map ⋯).prod (ν.map ⋯) = (μ.prod ν).map ⋯

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceMeasurableSpaceMeasurableSpace