Theorems · Theorem · measure theory

MeasureTheory.Measure.prod_sum_left

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ι : Type u_4}
  (m : ι → MeasureTheory.Measure α) (μ : MeasureTheory.Measure β) [MeasureTheory.SFinite μ],
  (MeasureTheory.Measure.sum m).prod μ = MeasureTheory.Measure.sum fun i => (m i).prod μ

Defined in

Mathlib.MeasureTheory.Measure.Prod

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceMeasureTheory.SFinite