cos — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem cos (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') x :=
  (Real.hasStrictDerivAt_cos (f x)).comp x hf

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