English
The map arg, composed with the inclusion, together with the exp map, defines a partial equivalence between Circle and ℝ with source univ and target Ioc(-π, π].
Русский
Отображение arg, с композицией включения и отображением exp, образуют частичное эквивалентное отображение между Circle и ℝ соSources: всe множествe, Target: Ioc(-π, π].
LaTeX
$$$$\\text{argPartialEquiv} : \\text{PartialEquiv Circle } \\mathbb{R},\\ \\, (toFun = arg \\circ (\\uparrow),\\ invFun = \\exp,\\ source = \\text{univ},\\ target = \\mathrm{Ioc}(-\\pi, \\pi)).$$$$
Lean4
/-- `Complex.arg ∘ (↑)` and `expMapCircle` define a partial equivalence between `circle` and `ℝ`
with `source = Set.univ` and `target = Set.Ioc (-π) π`. -/
@[simps -fullyApplied]
noncomputable def argPartialEquiv : PartialEquiv Circle ℝ
where
toFun := arg ∘ (↑)
invFun := exp
source := univ
target := Ioc (-π) π
map_source' _ _ := ⟨neg_pi_lt_arg _, arg_le_pi _⟩
map_target' := mapsTo_univ _ _
left_inv' z _ := exp_arg z
right_inv' _ hx := arg_exp hx.1 hx.2
