volume_preserving_piFinTwo — Mathlib

English

For a two-index finite product α: Fin 2 → Type, the piFinTwo equivalence is volume-preserving with respect to the product measure and the product volume.

Русский

Для двухиндексного произведения πFinTwo эквивалентность сохраняет объём относительно произведения мер и объёма.

LaTeX

$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.piFinTwo}(\alpha)\bigr)\; \mathrm{volume}\; \mathrm{volume} $$$

Lean4

theorem volume_preserving_piFinTwo (α : Fin 2 → Type u) [∀ i, MeasureSpace (α i)]
    [∀ i, SigmaFinite (volume : Measure (α i))] : MeasurePreserving (MeasurableEquiv.piFinTwo α) volume volume :=
  measurePreserving_piFinTwo _

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