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{derivWithin}(\\cosh \\circ f)\\ s\\ x = \\sinh(f(x)) \\cdot \\text{derivWithin}(f\\ s)\\ x$$$

Lean4

theorem cosh (hf : HasDerivAt f f' x) : HasDerivAt (fun x => Real.cosh (f x)) (Real.sinh (f x) * f') x :=
  (Real.hasDerivAt_cosh (f x)).comp x hf

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