English
For x ≠ 0, the map z ↦ arg z, viewed as Real.Angle, is continuous at x.
Русский
Для любого x ≠ 0 отображение z ↦ arg z, рассматриваемое как Real.Angle, непрерывно в точке x.
LaTeX
$$$$\\forall x \\in \\mathbb{C}, x \\neq 0 \Rightarrow \\text{ContinuousAt}((\\mathrm{Real.Angle}.coe) \\circ \\arg)(x).$$$$
Lean4
theorem continuousAt_arg_coe_angle (h : x ≠ 0) : ContinuousAt ((↑) ∘ arg : ℂ → Real.Angle) x :=
by
by_cases hs : x ∈ slitPlane
· exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs)
· rw [← Function.comp_id (((↑) : ℝ → Real.Angle) ∘ arg),
(funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ← Function.comp_assoc]
refine ContinuousAt.comp ?_ continuous_neg.continuousAt
suffices ContinuousAt (Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π) (-x) by
rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this
have ha : Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π = fun z => (arg z : Real.Angle) + π :=
by
rw [Function.update_eq_iff]
exact ⟨by simp, fun z hz => arg_neg_coe_angle hz⟩
rw [ha]
replace hs := mem_slitPlane_iff.mpr.mt hs
push_neg at hs
refine (Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg (Or.inl ?_))).add continuousAt_const
rw [neg_re, neg_pos]
exact hs.1.lt_of_ne fun h0 => h (Complex.ext_iff.2 ⟨h0, hs.2⟩)
