arg_eq_nhds_of_re_neg_of_im_neg — 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_neg (hx_re : x.re < 0) (hx_im : x.im < 0) :
    arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / ‖x‖) - π :=
  by
  suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ y.im < 0 from
    h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_neg hy.1 hy.2
  refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ x.im < 0)
  exact IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_im continuous_zero)

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