rexp'

Mathlib.Analysis.SpecialFunctions.ExpDeriv

URI: https://scilib.ai/kg/mathlib#AnalyticAt.rexp'

English

If fa is analytic at x, then exp ∘ f is analytic at x (rexp').

Русский

Если fa аналитична в x, то exp∘f аналитична в x (вариант).

LaTeX

$$$ \operatorname{AnalyticAt}_{\mathbb{R}} f x \Rightarrow \operatorname{AnalyticAt}_{\mathbb{R}} (\exp \circ f) x$$$

Lean4

/-- `exp ∘ f` is analytic -/
@[fun_prop]
theorem rexp' {x : E} (fa : AnalyticAt ℝ f x) : AnalyticAt ℝ (fun z ↦ exp (f z)) x :=
  fa.rexp

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

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

Разделы

Аффилиация

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