csinh

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

URI: https://scilib.ai/kg/mathlib#ContDiffAt.csinh

English

If f is ContDiffAt at x, then sinh(f) is ContDiffAt at x.

Русский

Если f ∈ ContDiffAt в x, то sinh(f) ∈ ContDiffAt в x.

LaTeX

$$$$ \text{ContDiffAt}_{\mathbb{C}}^{n}(f,x) \Rightarrow \text{ContDiffAt}_{\mathbb{C}}^{n}(\sinh(f),x). $$$$

Lean4

theorem csinh {n} (hf : ContDiffAt ℂ n f x) : ContDiffAt ℂ n (fun x => Complex.sinh (f x)) x :=
  Complex.contDiff_sinh.contDiffAt.comp x hf

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

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

Разделы

Аффилиация

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