tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero

English

For z with Re(z) < 0 and Im(z) = 0, Tendsto log along Im ≥ 0 approaches log|z| + π i.

Русский

Для z с Re(z) < 0 и Im(z) = 0, при подходе вдоль Im ≥ 0 логарифм стремится к log|z| + πi.

LaTeX

$$$\forall z:\, \mathrm{Re}(z) < 0,\ \mathrm{Im}(z) = 0:\; \mathrm{Tendsto}\log(\mathcal{N}_{z}^{\{w: w.im\ge 0\}}) \to \log \lVert z \rVert + \pi i$$$

Lean4

theorem tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :
    Tendsto log (𝓝[{z : ℂ | 0 ≤ z.im}] z) (𝓝 <| Real.log ‖z‖ + π * I) := by
  simpa only [log, arg_eq_pi_iff.2 ⟨hre, him⟩] using (continuousWithinAt_log_of_re_neg_of_im_zero hre him).tendsto

Похожие утверждения