measurableEquivRealMixedSpacePolarSpace

English

There exists a measurable equivalence between realMixedSpace K and polarSpace K.

Русский

Существует измеримое эквивалентное отображение между realMixedSpace K и polarSpace K.

LaTeX

$$$\\exists\\, \\text{measurableEquivRealMixedSpacePolarSpace}(K) : \\text{realMixedSpace}(K) \\simeq_m \\text{polarSpace}(K)$$$

Lean4

/-- The measurable equivalence between the `realMixedSpace` and the `polarSpace`. It is actually an
homeomorphism, see `homeoRealMixedSpacePolarSpace`, but defining it in this way makes it easier
to prove that it is volume preserving, see `volume_preserving_homeoRealMixedSpacePolarSpace`.
-/
def measurableEquivRealMixedSpacePolarSpace : realMixedSpace K ≃ᵐ polarSpace K :=
  MeasurableEquiv.trans (prodCongr (refl _) (arrowProdEquivProdArrow ℝ ℝ _)) <|
    MeasurableEquiv.trans prodAssoc.symm <|
      MeasurableEquiv.trans
        (prodCongr
          (prodCongr (refl _) (arrowCongr' (Equiv.subtypeEquivRight (fun _ ↦ not_isReal_iff_isComplex.symm)) (refl _)))
          (refl _))
        (prodCongr (piEquivPiSubtypeProd (fun _ ↦ ℝ) _).symm (refl _))

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