cos — Mathlib

English

If f has a derivative within s at x, then the derivative within s of cos(f(x)) at x equals -sin(f(x)) times the derivative within s of f at x.

Русский

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

LaTeX

$$$\\text{derivWithin}(\\cos \\circ f)\,s\,x = -\\sin(f(x)) \\cdot \\text{derivWithin}(f\\,s)\,x,$$$

Lean4

theorem cos (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') s x :=
  (Real.hasDerivAt_cos (f x)).comp_hasDerivWithinAt x hf

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