polarSpaceCoord — Mathlib

English

The inverse polar-space coord. map is measurable.

Русский

Обратное отображение полярной пространственной координаты измеримо.

LaTeX

$$$\\mathrm{Measurable}((\\mathrm{polarSpaceCoord}(K)).\\mathrm{symm})$$$

Lean4

/-- The polar coordinate open partial homeomorphism between the mixed space `ℝ^r₁ × ℂ^r₂` and the polar
space `ℝ^(r₁ + r₂) × ℝ^r₂` defined by sending `x` to `x w` or `‖x w‖` depending on whether `w` is
real or complex for the first component, and to `Arg (x w)`, `w` complex, for the second component.
-/
@[simps!]
def polarSpaceCoord [NumberField K] : OpenPartialHomeomorph (mixedSpace K) (polarSpace K) :=
  (mixedEmbedding.polarCoord K).transHomeomorph (homeoRealMixedSpacePolarSpace K)

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