arg_eq_nhds_of_re_neg_of_im_pos — Mathlib

English

If Re z < 0 and Im z > 0, then arg z equals Real.arcsin((-z).im / |z|) + π in a neighborhood of z.

Русский

Если Re z < 0 и Im z > 0, то в окрестности z аргумент z равен Real.arcsin((-z).im / |z|) + π.

LaTeX

$$$ (\operatorname{Re} z < 0) \land (\operatorname{Im} z > 0) \Rightarrow\ arg z =^\to (x \mapsto \operatorname{arcsin}((-x).\mathrm{im} / \|x\|) + \pi) $$

Lean4

theorem arg_eq_nhds_of_re_neg_of_im_pos (hx_re : x.re < 0) (hx_im : 0 < x.im) :
    arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / ‖x‖) + π :=
  by
  suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ 0 < y.im from
    h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_nonneg hy.1 hy.2.le
  refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ 0 < x.im)
  exact IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_zero continuous_im)

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