volume_preserving_homeoRealMixedSpacePolarSpace

English

The homeomorphism between realMixedSpace and polarSpace preserves volume.

Русский

Гомеоморфизм сохраняет объём.

LaTeX

$$$\\text{volume-preserving}(\\mathrm{homeoRealMixedSpacePolarSpace}(K))$$$

Lean4

theorem volume_preserving_homeoRealMixedSpacePolarSpace [NumberField K] :
    MeasurePreserving (homeoRealMixedSpacePolarSpace K) :=
  ((MeasurePreserving.id volume).prod (volume_measurePreserving_arrowProdEquivProdArrow ℝ ℝ _)).trans <|
    (volume_preserving_prodAssoc.symm).trans <|
      (((MeasurePreserving.id volume).prod (volume_preserving_arrowCongr' _ (MeasurableEquiv.refl ℝ) (.id volume))).prod
            (.id volume)).trans <|
        ((volume_preserving_piEquivPiSubtypeProd (fun _ : InfinitePlace K ↦ ℝ) (fun w ↦ IsReal w)).symm).prod
          (.id volume)

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