volume_preserving_equiv_pi — Mathlib

English

The measurable equivalence measurableEquivPi preserves volume in the sense that it is volume-preserving between the domain and the product space.

Русский

Измеримая эквивалентность measurableEquivPi сохраняет меру объема между областью и пространством произведения.

LaTeX

$$$\text{MeasurePreserving} \;\text{measurableEquivPi}$$$

Lean4

theorem volume_preserving_equiv_pi : MeasurePreserving measurableEquivPi :=
  by
  convert (measurableEquivPi.symm.measurable.measurePreserving volume).symm
  rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar, measurableEquivPi,
    Homeomorph.toMeasurableEquiv_symm_coe, ContinuousLinearEquiv.coe_symm_toHomeomorph, Basis.map_addHaar, eq_comm]
  exact (Basis.addHaar_eq_iff _ _).mpr Complex.orthonormalBasisOneI.volume_parallelepiped

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