continuousAt_clog — Mathlib

English

There exists an integer n such that log(exp z) = z + n·(2πi).

Русский

Существует целое n такое, что log(exp z) = z + n·(2πi).

LaTeX

$$$\exists n \in \mathbb{Z},\ log(\exp z) = z + n \cdot (2 \pi i)$$$

Lean4

theorem continuousAt_clog {x : ℂ} (h : x ∈ slitPlane) : ContinuousAt log x :=
  by
  refine ContinuousAt.add ?_ ?_
  · refine continuous_ofReal.continuousAt.comp ?_
    refine (Real.continuousAt_log ?_).comp continuous_norm.continuousAt
    exact norm_ne_zero_iff.mpr <| slitPlane_ne_zero h
  · have h_cont_mul : Continuous fun x : ℂ => x * I := continuous_id'.mul continuous_const
    refine h_cont_mul.continuousAt.comp (continuous_ofReal.continuousAt.comp ?_)
    exact continuousAt_arg h

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