cosh — Mathlib

English

If f has a derivative within s at x, then the derivative within s of cosh(f(x)) is sinh(f(x)) times the derivative within s of f.

Русский

Если f имеет производную внутри s в точке x, то производная cosh(f(x)) внутри s в x равна sinh(f(x)) умножить на производную внутри s от f.

LaTeX

$$$\\text{HasDerivWithinAt}(\\cosh \\circ f)\\ s\\ x = \\cosh'(f(x)) \\cdot \\text{HasDerivWithinAt}(f\\ s)\\ x$$$

Lean4

theorem cosh (hf : HasDerivWithinAt f f' s x) :
    HasDerivWithinAt (fun x => Real.cosh (f x)) (Real.sinh (f x) * f') s x :=
  (Real.hasDerivAt_cosh (f x)).comp_hasDerivWithinAt x hf

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