volume_preserving_funUnique — Mathlib

English

For a type α and a type β with a measure space structure, if α is unique, then the canonical funUnique α β is volume-preserving between the constant product measure and volume.

Русский

Для типа α и типа β с пространством меры, если α уникален, то каноническая функция funUnique α β сохраняет объём между соответствующей произведением меры и объёмом.

LaTeX

$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.funUnique}(\alpha,\beta)\bigr)\; \mathrm{volume}\; \mathrm{volume} $$$

Lean4

theorem volume_preserving_funUnique (α : Type u) (β : Type v) [Unique α] [MeasureSpace β] :
    MeasurePreserving (MeasurableEquiv.funUnique α β) volume volume :=
  measurePreserving_funUnique volume α

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