Theorems · Theorem · measure theory

MeasureTheory.measurePreserving_sumPiEquivProdPi_symm

∀ {ι : Type u_1} {ι' : Type u_2} [inst : Fintype ι] [inst_1 : Fintype ι'] {X : ι ⊕ ι' → Type u_4}
  {m : (i : ι ⊕ ι') → MeasurableSpace (X i)} (μ : (i : ι ⊕ ι') → MeasureTheory.Measure (X i))
  [∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm)
    ((MeasureTheory.Measure.pi fun i => μ (Sum.inl i)).prod (MeasureTheory.Measure.pi fun i => μ (Sum.inr i)))
    (MeasureTheory.Measure.pi μ)

Defined in

Mathlib.MeasureTheory.Constructions.Pi

Cited by

3 results in Mathlib

Foundations

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

Assumes

FintypeFintypeMeasureTheory.SigmaFinite