Theorems · Theorem · measure theory

MeasureTheory.Measure.prod_prod

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (s : Set α) (t : Set β), (μ.prod ν) (s ×ˢ t) = μ s * ν t

The product measure of the product of two sets is the product of their measures. Note that we do not need the sets to be measurable.

Defined in

Mathlib.MeasureTheory.Measure.Prod

Cited by

38 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceMeasureTheory.SFinite