English
For every z in the slit plane, the argument function is continuous at z.
Русский
Для каждой точки z на слитной плоскости функция аргумента непрерывна в точке z.
LaTeX
$$$ \forall z \in \text{slitPlane},\; \operatorname{ContinuousAt}(\operatorname{arg}, z). $$$
Lean4
theorem continuousAt_arg (h : x ∈ slitPlane) : ContinuousAt arg x :=
by
have h₀ : ‖x‖ ≠ 0 := by
rw [norm_ne_zero_iff]
exact slitPlane_ne_zero h
rw [mem_slitPlane_iff, ← lt_or_lt_iff_ne] at h
rcases h with (hx_re | hx_im | hx_im)
exacts
[(Real.continuousAt_arcsin.comp (continuous_im.continuousAt.div continuous_norm.continuousAt h₀)).congr
(arg_eq_nhds_of_re_pos hx_re).symm,
(Real.continuous_arccos.continuousAt.comp
(continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).neg.congr
(arg_eq_nhds_of_im_neg hx_im).symm,
(Real.continuous_arccos.continuousAt.comp (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).congr
(arg_eq_nhds_of_im_pos hx_im).symm]
