deriv_sinh — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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