measurePreserving_measurableEquiv

English

The measurable equivalence defined by an orthonormal basis is measure-preserving with respect to volume.

Русский

Измеримое эквивалентное отображение, задаваемое ортонормированным базисом, сохраняет меру объема.

LaTeX

$$$b.measurableEquiv \\text{ preserves } volume$.$$

Lean4

/-- The measurable equivalence defined by an orthonormal basis is volume preserving. -/
theorem measurePreserving_measurableEquiv (b : OrthonormalBasis ι ℝ F) :
    MeasurePreserving b.measurableEquiv volume volume :=
  by
  convert (b.measurableEquiv.symm.measurable.measurePreserving _).symm
  rw [← (EuclideanSpace.basisFun ι ℝ).addHaar_eq_volume]
  erw [MeasurableEquiv.coe_toEquiv_symm, Basis.map_addHaar _ b.repr.symm.toContinuousLinearEquiv]
  exact b.addHaar_eq_volume.symm

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