analyticOn_rexp

Mathlib.Analysis.SpecialFunctions.ExpDeriv

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

English

The real exponential function exp is analytic on all of ℝ.

Русский

Функция exp на ℝ аналитична вовсе.

LaTeX

$$$ \operatorname{AnalyticOn}_{\mathbb{R}} \exp (\mathbb{R})$$$

Lean4

/-- The function `Real.exp` is real analytic. -/
theorem analyticOn_rexp : AnalyticOn ℝ exp univ :=
  analyticOnNhd_rexp.analyticOn

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

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

Разделы

Аффилиация

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