mixedSpaceToRealMixedSpace — Mathlib

English

The real mixed space is the product of real embeddings and complex embeddings treated as pairs.

Русский

Реальное смешанное пространство является произведением по действительным вложениям и по комплексным вложениям, рассматриваемым как пары.

LaTeX

$$$\\text{realMixedSpace}(K) = \\bigl( \\{ w : \\mathrm{InfinitePlace}(K) \\mid \\mathrm{IsReal}(w) \\} \\to \\mathbb{R} \\bigr) \\times \\bigl( \\{ w : \\mathrm{InfinitePlace}(K) \\mid \\mathrm{IsComplex}(w) \\} \\to \\mathbb{R} \\times \\mathbb{R} \\bigr).$$$

Lean4

/-- The natural homeomorphism between the mixed space `ℝ^r₁ × ℂ^r₂` and the real mixed space
`ℝ^r₁ × (ℝ × ℝ)^r₂`.
-/
noncomputable def mixedSpaceToRealMixedSpace : mixedSpace K ≃ₜ realMixedSpace K :=
  (Homeomorph.refl _).prodCongr <| .piCongrRight fun _ ↦ Complex.equivRealProdCLM.toHomeomorph

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