analyticAt_cexp — Mathlib

English

The exp function is analytic within any set; in particular exp is analytic within any neighborhood of every point.

Русский

Функция exp аналитична внутри любой области; в частности, аналитична в окрестности каждой точки.

LaTeX

$$$ \text{AnalyticWithinAt } \mathbb{C} (\exp) (s) x $$$

Lean4

/-- The function `Complex.exp` is complex analytic. -/
@[fun_prop]
theorem analyticAt_cexp : AnalyticAt ℂ exp z :=
  analyticOnNhd_cexp z (mem_univ _)

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