continuousWithinAt_log_of_re_neg_of_im_zero

English

If Re(z) < 0 and Im(z) = 0, log is continuous within the set {w ∈ ℂ : 0 ≤ Im(w)} at z.

Русский

Если Re(z) < 0 и Im(z) = 0, то log непрерывна внутри множества {w ∈ ℂ : Im(w) ≥ 0} в точке z.

LaTeX

$$$\forall z:\, \mathrm{Re}(z) < 0,\ \mathrm{Im}(z) = 0:\; \operatorname{ContinuousWithinAt} \log \{w \in \mathbb{C} \mid 0 \le \mathrm{Im}(w)\} \; z$$$

Lean4

theorem continuousWithinAt_log_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :
    ContinuousWithinAt log {z : ℂ | 0 ≤ z.im} z :=
  by
  convert
    (continuous_ofReal.continuousAt.comp_continuousWithinAt (continuous_norm.continuousWithinAt.log _)).tendsto.add
      ((continuous_ofReal.continuousAt.comp_continuousWithinAt <|
            continuousWithinAt_arg_of_re_neg_of_im_zero hre him).mul
        tendsto_const_nhds) using
    1
  lift z to ℝ using him
  simpa using hre.ne

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