deriv_cos — Mathlib

English

If f is differentiable at x, then the derivative of cos(f(x)) at x is -sin(f(x)) f'(x).

Русский

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

LaTeX

$$$\\frac{d}{dx}\\bigl(\\cos(f(x))\\bigr) = -\\sin(f(x)) \\cdot \\frac{d}{dx}f(x).$$$

Lean4

@[simp]
theorem deriv_cos (hc : DifferentiableAt ℝ f x) : deriv (fun x => Real.cos (f x)) x = -Real.sin (f x) * deriv f x :=
  hc.hasDerivAt.cos.deriv

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