analyticAt_rexp

Mathlib.Analysis.SpecialFunctions.ExpDeriv

URI: https://scilib.ai/kg/mathlib#analyticAt_rexp

English

The exponential function exp is analytic at every point x ∈ ℝ.

Русский

Экспонента аналитична в любой точке x ∈ ℝ.

LaTeX

$$$ \operatorname{AnalyticAt}_{\mathbb{R}} \exp x $$$

Lean4

/-- The function `Real.exp` is real analytic. -/
@[fun_prop]
theorem analyticAt_rexp : AnalyticAt ℝ exp x :=
  analyticOnNhd_rexp x (mem_univ _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru