analyticOnNhd_rexp — Mathlib

English

The real exponential function is analytic on a neighborhood of every point (in particular on all of ℝ).

Русский

Функция экспоненты на вещественной оси аналитична в окрестности любой точки (и на всей ℝ).

LaTeX

$$$ \operatorname{AnalyticOnNhd}_{\mathbb{R}} \exp \mathbb{R}$$$

Lean4

/-- The function `Real.exp` is real analytic. -/
theorem analyticOnNhd_rexp : AnalyticOnNhd ℝ exp univ :=
  by
  rw [Real.exp_eq_exp_ℝ]
  exact fun x _ ↦ NormedSpace.exp_analytic x

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