Theorems · Definition · measure theory

MeasureTheory.Measure.prod

{α : Type u_4} →
  {β : Type u_5} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → MeasureTheory.Measure α → MeasureTheory.Measure β → MeasureTheory.Measure (α × β)

The binary product of measures. They are defined for arbitrary measures, but we basically prove all properties under the assumption that at least one of them is s-finite.

Defined in

Mathlib.MeasureTheory.Measure.Prod

Cited by

353 results in Mathlib

Foundations

Depth 213 from the axioms, rests on 5,162 definitions · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSpace