The argument of a complex number. #
We define arg : ℂ → ℝ
, returning a real number in the range (-π, π],
such that for x ≠ 0
, sin (arg x) = x.im / x.abs
and cos (arg x) = x.re / x.abs
,
while arg 0
defaults to 0
@[simp]
An alternative description of the slit plane as consisting of nonzero complex numbers whose argument is not π.
theorem
Complex.tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero
{z : ℂ}
(hre : z.re < 0)
(him : z.im = 0)
:
Filter.Tendsto Complex.arg (nhdsWithin z {z : ℂ | z.im < 0}) (nhds (-Real.pi))
theorem
Complex.continuousWithinAt_arg_of_re_neg_of_im_zero
{z : ℂ}
(hre : z.re < 0)
(him : z.im = 0)
:
ContinuousWithinAt Complex.arg {z : ℂ | 0 ≤ z.im} z
theorem
Complex.tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero
{z : ℂ}
(hre : z.re < 0)
(him : z.im = 0)
:
Filter.Tendsto Complex.arg (nhdsWithin z {z : ℂ | 0 ≤ z.im}) (nhds Real.pi)