measurePreserving — Mathlib

English

Every linear isometry on a real finite-dimensional Hilbert space preserves volume (hence measure).

Русский

Любая линейная изометрия на вещественном конечномерном гильбертовом пространстве сохраняет объём (а значит и меру).

LaTeX

$$$f : E \\simeq_{\\mathrm{lin}} F \\Rightarrow f$ is measure-preserving with respect to volume.$$

Lean4

/-- Every linear isometry on a real finite-dimensional Hilbert space is measure-preserving. -/
theorem measurePreserving (f : E ≃ₗᵢ[ℝ] F) : MeasurePreserving f :=
  by
  refine ⟨f.continuous.measurable, ?_⟩
  rcases exists_orthonormalBasis ℝ E with ⟨w, b, _hw⟩
  erw [← OrthonormalBasis.addHaar_eq_volume b, ← OrthonormalBasis.addHaar_eq_volume (b.map f),
    Basis.map_addHaar _ f.toContinuousLinearEquiv]
  congr

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