deriv_cosh — Mathlib

English

If f is differentiable at x, then the derivative of cosh(f(x)) at x is sinh(f(x)) times f'(x).

Русский

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

LaTeX

$$$\\frac{d}{dx}\\bigl(\\cosh(f(x))\\bigr) = \\sinh(f(x)) \\cdot f'(x).$$$

Lean4

@[simp]
theorem deriv_cosh (hc : DifferentiableAt ℝ f x) : deriv (fun x => Real.cosh (f x)) x = Real.sinh (f x) * deriv f x :=
  hc.hasDerivAt.cosh.deriv

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