arg_eq_nhds_of_re_pos — Mathlib

English

Let z be a complex number with Re z > 0. Then arg z is eventually equal to Real.arcsin(Im z / |z|) near z.

Русский

Пусть z имеет положительную вещественную часть. Тогда в окрестности z аргумент z совпадает с Real.arcsin(Im z / |z|) для близких точек.

LaTeX

$$$ 0 < \operatorname{Re} z \Rightarrow \ arg z =^\to 𝓝_z \ (x \mapsto \operatorname{arcsin}\left(\frac{\operatorname{Im} x}{\|x\|} \right)) $$$

Lean4

theorem arg_eq_nhds_of_re_pos (hx : 0 < x.re) : arg =ᶠ[𝓝 x] fun x => Real.arcsin (x.im / ‖x‖) :=
  ((continuous_re.tendsto _).eventually (lt_mem_nhds hx)).mono fun _ hy => arg_of_re_nonneg hy.le

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