homeoRealMixedSpacePolarSpace — Mathlib

English

There is a homeomorphism between realMixedSpace K and polarSpace K.

Русский

Существует гомеморфизм между realMixedSpace K и polarSpace K.

LaTeX

$$$\\text{homeoRealMixedSpacePolarSpace}(K) : \\text{realMixedSpace}(K) \\simeq_t \\text{polarSpace}(K)$$$

Lean4

/-- The homeomorphism between the `realMixedSpace` and the `polarSpace`.
-/
def homeoRealMixedSpacePolarSpace : realMixedSpace K ≃ₜ polarSpace K :=
  {
    measurableEquivRealMixedSpacePolarSpace
      K with
    continuous_toFun :=
      by
      change
        Continuous fun x : realMixedSpace K ↦
          (fun w ↦ if hw : w.IsReal then x.1 ⟨w, hw⟩ else (x.2 ⟨w, not_isReal_iff_isComplex.mp hw⟩).1, fun w ↦
            (x.2 w).2)
      refine .prodMk (continuous_pi fun w ↦ ?_) (by fun_prop)
      split_ifs <;> fun_prop
    continuous_invFun :=
      by
      change Continuous fun x : polarSpace K ↦ (⟨fun w ↦ x.1 w.val, fun w ↦ ⟨x.1 w.val, x.2 w⟩⟩ : realMixedSpace K)
      fun_prop }

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