ccosh — Mathlib

English

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

Русский

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

LaTeX

$$$$ Df_{s}(x) \;\text{for } (\cosh \circ f)_{s}(x) = \sinh(f(x)) \cdot f'_{s}(x). $$$$

Lean4

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

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