Theorems · Theorem · measure theory

MeasureTheory.ProbabilityMeasure.map_fst_prod

∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β), (μ.prod ν).map ⋯ = μ

The first marginal of a product probability measure is the first probability measure.

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace