volume_preserving_prodAssoc — Mathlib

English

The associativity isomorphism between triple product volume measures is measure-preserving.

Русский

Ассоциативное отображение между объемами произведений тройки мер сохраняет меру.

LaTeX

$$MeasurePreserving(prodAssoc : ((α1 × β1) × γ1) ≃ᵐ (α1 × (β1 × γ1)), volume, volume)$$

Lean4

theorem _root_.MeasureTheory.volume_preserving_prodAssoc {α₁ β₁ γ₁ : Type*} [MeasureSpace α₁] [MeasureSpace β₁]
    [MeasureSpace γ₁] [SFinite (volume : Measure β₁)] [SFinite (volume : Measure γ₁)] :
    MeasurePreserving (MeasurableEquiv.prodAssoc : (α₁ × β₁) × γ₁ ≃ᵐ α₁ × β₁ × γ₁) :=
  MeasureTheory.measurePreserving_prodAssoc volume volume volume

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