measurePreserving_repr_symm — Mathlib

English

The inverse of the representation map preserves volume as a measurable equivalence.

Русский

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

LaTeX

$$$b.repr.symm$ preserves volume.$$

Lean4

theorem measurePreserving_repr_symm (b : OrthonormalBasis ι ℝ F) : MeasurePreserving b.repr.symm volume volume :=
  b.measurePreserving_measurableEquiv.symm

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