English
If f is differentiable within a set s at x and s has a unique differentiable point at x, then the derivative within s of cosh(f) equals sinh(f(x)) times the derivative within s of f.
Русский
Если f дифференцируема внутри множества s в точке x и в точке x существует единственная точка дифференцирования, то производная внутри s функции cosh(f(x)) равна sinh(f(x)) умножить на производную внутри s f.
LaTeX
$$$fderivWithin\\,\\mathbb{R}(\\cosh(f(x)))\\, s\\, x = \\sinh(f(x)) \\cdot fderivWithin\\,\\mathbb{R} f\\, s\\, x$$$
Lean4
theorem fderivWithin_cosh (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
fderivWithin ℝ (fun x => Real.cosh (f x)) s x = Real.sinh (f x) • fderivWithin ℝ f s x :=
hf.hasFDerivWithinAt.cosh.fderivWithin hxs
