fderiv_sinh — Mathlib

English

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

Русский

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

LaTeX

$$$\forall E\ [\text{NormedAddCommGroup } E]\ [\text{NormedSpace } \mathbb{R} E],\ {f: E \to \mathbb{R}},\ (\text{DifferentiableAt } \mathbb{R} f\ x)\Rightarrow \\ fderiv\mathbb{R}(\lambda x: \sinh(f x)) x = \cosh(f x) \cdot fderiv\mathbb{R} f x.$$$

Lean4

@[simp]
theorem fderiv_sinh (hc : DifferentiableAt ℝ f x) :
    fderiv ℝ (fun x => Real.sinh (f x)) x = Real.cosh (f x) • fderiv ℝ f x :=
  hc.hasFDerivAt.sinh.fderiv

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