English
If Re z < 0 and Im z = 0, then arg x tends to -π when x tends to z within the lower half-plane.
Русский
Если Re z < 0 и Im z = 0, то аргумент x стремится к −π при стремлении x к z внутри нижней полуплоскости.
LaTeX
$$$ (\operatorname{Re} z < 0) \land (\operatorname{Im} z = 0) \Rightarrow\ \operatorname{Tendsto}(\operatorname{arg}, \mathcal{N}[{z : \mathbb{C} \mid z.\mathrm{im} < 0}] z, \mathcal{N}(-\pi)) $$$
Lean4
theorem tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :
Tendsto arg (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π)) :=
by
suffices H : Tendsto (fun x : ℂ => Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
by
refine H.congr' ?_
have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds this] with _ him hre
rw [arg, if_neg hre.not_ge, if_neg him.not_ge]
convert
(Real.continuousAt_arcsin.comp_continuousWithinAt
((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
continuous_norm.continuousWithinAt _)).sub_const
π using
1
· simp [him]
· lift z to ℝ using him
simpa using hre.ne
