csinh — Mathlib

English

If f is differentiable at x with derivative f', then the derivative of sinh(f) at x is cosh(f(x))·f'.

Русский

Если f дифференцируема в x с производной f', то производная sinh(f) в x равна cosh(f(x))·f'.

LaTeX

$$$$ HasFDerivAt_{\mathbb{C}} f f'(x) \Rightarrow HasFDerivAt_{\mathbb{C}} (\sinh(f)) (\cosh(f(x))\cdot f')(x). $$$$

Lean4

theorem csinh (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) • f') x :=
  (Complex.hasDerivAt_sinh (f x)).comp_hasFDerivAt x hf

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