measurePreserving_sumPiEquivProdPi

English

There is a measure-preserving map from the sum-Pi construction to the product of Pi-structures.

Русский

Существет мапа сохраняющая меру между конструкцией sumPi и произведением Pi-структур.

LaTeX

$$measurePreserving_sumPiEquivProdPi (X) :$$

Lean4

theorem measurePreserving_sumPiEquivProdPi {X : ι ⊕ ι' → Type*} {_m : ∀ i, MeasurableSpace (X i)}
    (μ : ∀ i, Measure (X i)) [∀ i, SigmaFinite (μ i)] :
    MeasurePreserving (MeasurableEquiv.sumPiEquivProdPi X) (Measure.pi μ)
      ((Measure.pi fun i => μ (.inl i)).prod (Measure.pi fun i => μ (.inr i))) :=
  measurePreserving_sumPiEquivProdPi_symm μ |>.symm

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