cos — Mathlib

English

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

Русский

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

LaTeX

$$$DWithin_s(\\cos(f(x))) = (-\\sin(f(x))) \\cdot DWithin_s(f(x))$$$

Lean4

theorem cos (hf : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (fun x => Real.cos (f x)) (-Real.sin (f x) • f') s x :=
  (Real.hasDerivAt_cos (f x)).comp_hasFDerivWithinAt x hf

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