volume_measurePreserving_sumPiEquivProdPi_symm

English

The symmetric version of the measure-preserving equivalence between sum-Pi and Pi-Prod-Pi constructions preserves measure.

Русский

Симметрическая версия сохраняет меру при эквивалентности между sumPi и PiProdPi.

LaTeX

$$measurePreserving_sumPiEquivProdPi_symm (X) :$$

Lean4

theorem volume_measurePreserving_sumPiEquivProdPi_symm (X : ι ⊕ ι' → Type*) [∀ i, MeasureSpace (X i)]
    [∀ i, SigmaFinite (volume : Measure (X i))] :
    MeasurePreserving (MeasurableEquiv.sumPiEquivProdPi X).symm volume volume :=
  measurePreserving_sumPiEquivProdPi_symm (fun _ ↦ volume)

Похожие утверждения