csinh — Mathlib

English

If f is differentiableWithinAt s x, then sinh(f) is differentiableWithinAt s x with derivative cosh(f(x))•f'(x).

Русский

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

LaTeX

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

Lean4

theorem csinh (hf : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) • f') s x :=
  (Complex.hasDerivAt_sinh (f x)).comp_hasFDerivWithinAt x hf

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