polarSpaceCoord_target' — Mathlib

English

The target of polarSpaceCoord equals a product of unbounded real-interval sets reflecting real and complex places.

Русский

Множество значений polarSpaceCoord равно произведению соответствующих множества.

LaTeX

$$$\$polarSpaceCoord(K)\$.target = (\\mathrm Set.univ)^{\\pi} \\;\\times\\; (\\mathrm Set.univ)^{\\pi}$$$

Lean4

theorem polarSpaceCoord_target' [NumberField K] :
    (polarSpaceCoord K).target =
      (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ (Set.univ.pi fun _ ↦ Set.Ioo (-π) π) :=
  by
  ext
  simp_rw [polarSpaceCoord_target, Set.mem_preimage, homeoRealMixedSpacePolarSpace_symm_apply, Set.mem_prod,
    Set.mem_univ, true_and, Set.mem_univ_pi, Set.mem_ite_univ_left, not_isReal_iff_isComplex, Subtype.forall,
    Complex.polarCoord_target, Set.mem_prod, forall_and]

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