English
Let f be differentiable within a set s at a point x and x be a unique differentiability point for s. Then the derivative within s of sinh(f) at x equals cosh(f(x)) times the derivative within s of f at x.
Русский
Пусть f дифференцируема внутри множества s в точке x и x является точкой duyности для s. Тогда производная внутри s композиции sinh(f) в x равна cosh(f(x)) умножить на производную внутри s f в x.
LaTeX
$$$\\operatorname{derivWithin}(\\lambda y. \\operatorname{Real.sinh}(f(y)), s, x) = \\cosh(f(x)) \\cdot \\operatorname{derivWithin} f\\ s\\ x$$$
Lean4
theorem derivWithin_sinh (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
derivWithin (fun x => Real.sinh (f x)) s x = Real.cosh (f x) * derivWithin f s x :=
hf.hasDerivWithinAt.sinh.derivWithin hxs
