arg_eq_nhds_of_im_neg — Mathlib

English

If Im z < 0, then arg z equals - Real.arccos (Re z / |z|) in a neighborhood of z.

Русский

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

LaTeX

$$$ (\operatorname{Im} z < 0) \Rightarrow\ arg z =^\to (x \mapsto -\operatorname{arccos} (x.re / \|x\|)) $$$

Lean4

theorem arg_eq_nhds_of_im_neg (hz : im z < 0) : arg =ᶠ[𝓝 z] fun x => -Real.arccos (x.re / ‖x‖) :=
  ((continuous_im.tendsto _).eventually (gt_mem_nhds hz)).mono fun _ => arg_of_im_neg

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