cos — Mathlib

English

If f has a Frechet derivative f' at x, then the Frechet derivative of cos(f(x)) at x is -sin(f(x)) times f' as a linear map.

Русский

Если у f в точке x есть производная Фреше f', то производная Фреше от cos(f(x)) в x равна -sin(f(x)) умножить на f' как линейное отображение.

LaTeX

$$$D(\\cos(f))(x) = (-\\sin(f(x))) \\cdot f'\\,,$ where $f'$ is the Frechet derivative of $f$ at $x$.$$

Lean4

theorem cos (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) • f') x :=
  (Real.hasDerivAt_cos (f x)).comp_hasFDerivAt x hf

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