volume_preserving_finTwoArrow — Mathlib

English

For a Fin 2-indexed family α, the piFinTwo equivalence is measure-preserving between the product measure and the product of the two coordinate measures.

Русский

Для семейства с индексами Fin 2 эквивалентность piFinTwo сохраняет меру между произведением и произведением двух координатных мер.

LaTeX

$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.piFinTwo}(\alpha)\bigr)\; (\mathrm{Measure.pi}\, μ)\; ((μ_0).\mathrm{prod}(μ_1)) $$$

Lean4

theorem volume_preserving_finTwoArrow (α : Type u) [MeasureSpace α] [SigmaFinite (volume : Measure α)] :
    MeasurePreserving (@MeasurableEquiv.finTwoArrow α _) volume volume :=
  measurePreserving_finTwoArrow volume

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