English
There is a natural homeomorphism between AddCircle(2π) and Circle, given by the angle-to-circle map and its inverse given by the argument function; the forward map is θ ↦ toCircle θ and the inverse map is z ↦ arg z.
Русский
Существует естественный гомеоморфизм между AddCircle(2π) и Circle, задаваемый переходом угла в точку на окружности и обратной операцией через аргумент; переход вперёд: θ ↦ toCircle θ, обратный переход: z ↦ arg z.
LaTeX
$$$$ AddCircle(2\pi) \cong_t Circle. $$$$
Lean4
/-- The homeomorphism between `AddCircle (2 * π)` and `Circle`. -/
@[simps]
noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ Circle
where
toFun := Angle.toCircle
invFun := fun x ↦ arg x
left_inv := Angle.arg_toCircle
right_inv := Circle.exp_arg
continuous_toFun := continuous_coinduced_dom.mpr Circle.exp.continuous
continuous_invFun := by
rw [continuous_iff_continuousAt]
intro x
exact (continuousAt_arg_coe_angle x.coe_ne_zero).comp continuousAt_subtype_val
