cos — Mathlib

English

Let f have a strict derivative at x. Then the derivative of cos(f(x)) at x is -sin(f(x)) times the derivative of f at x, in the sense of the Fréchet derivative.

Русский

Пусть у функции f существует строгий предел производной в точке x. Тогда производная cos(f(x)) в точке x равна -sin(f(x)) умножить на производную f в x (по Фрете).

LaTeX

$$$D(\\cos(f(x))) = -\\sin(f(x)) \\cdot Df(x)$$$

Lean4

theorem cos (hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) • f') x :=
  (Real.hasStrictDerivAt_cos (f x)).comp_hasStrictFDerivAt x hf

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