argEquiv — Mathlib

English

The complex argument and the exponential map give a bijection between Circle and (-π, π].

Русский

Комплексный аргумент и экспонента дают биекцию между Circle и (-π, π].

LaTeX

$$$$\\text{argEquiv} : \\ Circle \\simeq Ioc(-\\pi, \\pi).$$$$

Lean4

/-- `Complex.arg` and `expMapCircle` define an equivalence between `circle` and `(-π, π]`. -/
@[simps -fullyApplied]
noncomputable def argEquiv : Circle ≃ Ioc (-π) π
    where
  toFun z := ⟨arg z, neg_pi_lt_arg _, arg_le_pi _⟩
  invFun := exp ∘ (↑)
  left_inv _ := argPartialEquiv.left_inv trivial
  right_inv x := Subtype.ext <| argPartialEquiv.right_inv x.2

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