rexp

Mathlib.Analysis.SpecialFunctions.ExpDeriv

URI: https://scilib.ai/kg/mathlib#AnalyticOn.rexp

English

If fs is AnalyticOn ℝ f s, then exp ∘ f is AnalyticOn ℝ on s.

Русский

Если f аналитична на s, то exp∘f аналитична на s.

LaTeX

$$$ \operatorname{AnalyticOn}_{\mathbb{R}} f s \Rightarrow \operatorname{AnalyticOn}_{\mathbb{R}} (\exp \circ f) s$$$

Lean4

theorem «rexp» (fs : AnalyticOn ℝ f s) : AnalyticOn ℝ (fun z ↦ exp (f z)) s :=
  analyticOnNhd_rexp.comp_analyticOn fs (mapsTo_univ _ _)

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

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

Разделы

Аффилиация

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