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