tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero

English

For x ≠ 0, the map z ↦ (arg z) considered as Real.Angle is continuous at x away from 0.

Русский

Для x ≠ 0 отображение z ↦ arg z, рассматриваемое как Real.Angle, непрерывно в точке x.

LaTeX

$$$$\\forall x \\in \\mathbb{C}, \\ x \\neq 0 \\Rightarrow \\text{ContinuousAt}((\\uparrow) \\circ \\arg)(x).$$$$

Lean4

theorem tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :
    Tendsto arg (𝓝[{z : ℂ | 0 ≤ z.im}] z) (𝓝 π) := by
  simpa only [arg_eq_pi_iff.2 ⟨hre, him⟩] using (continuousWithinAt_arg_of_re_neg_of_im_zero hre him).tendsto

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