English
If z is a negative real (Re z < 0, Im z = 0), then as you approach z from points with nonnegative imaginary part, arg(w) tends to π.
Русский
Если z является отрицательным действительным числом (Re z < 0, Im z = 0), то при подходе w к z по пути с Im w ≥ 0 аргумент w стремится к π.
LaTeX
$$$$\\text{If } \\operatorname{Re}(z) < 0 \\text{ and } \\operatorname{Im}(z) = 0, \\quad \\operatorname{Tendsto} \\arg(w) \\\\to \\mathcal{N}_\\pi \\text{ as } w \\to z \\text{ with } \\operatorname{Im}(w) \\ge 0.$$$$
Lean4
/-- `arg` returns values in the range (-π, π], such that for `x ≠ 0`,
`sin (arg x) = x.im / x.abs` and `cos (arg x) = x.re / x.abs`,
`arg 0` defaults to `0` -/
noncomputable def arg (x : ℂ) : ℝ :=
if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
else if 0 ≤ x.im then Real.arcsin ((-x).im / ‖x‖) + π else Real.arcsin ((-x).im / ‖x‖) - π
