continuous_exp — Mathlib

English

The complex exponential function exp: ℂ → ℂ is continuous on the entire plane.

Русский

Функция экспоненты exp: ℂ → ℂ непрерывна на всей плоскости.

LaTeX

$$$$ \\exp: \\mathbb{C} \\to \\mathbb{C} \\quad \\text{is continuous on } \\mathbb{C}. $$$$

Lean4

@[continuity]
theorem continuous_exp : Continuous exp :=
  continuous_iff_continuousAt.mpr fun x =>
    continuousAt_of_locally_lipschitz zero_lt_one (2 * ‖exp x‖)
      (fun y ↦ by
        convert locally_lipschitz_exp zero_le_one le_rfl x y using 2
        congr
        ring)

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