ccos — Mathlib

English

If a function f: E → ℂ has a derivative within a set s at x (represented by a linear map f'), then the derivative of the composite cos ∘ f at x within s is given by the chain rule: D(cos ∘ f)(x) = −sin(f(x)) · Df(x).

Русский

Если функция f: E → ℂ имеет производную внутри множества s в точке x, представленную линейным отображением f', то производная композиции cos ∘ f в точке x внутри s равна D(cos ∘ f)(x) = −sin(f(x)) · Df(x).

LaTeX

$$$f'':=f'\\quad\\Rightarrow\\quad \\mathrm{D}(\cos\\circ f)(x) = -\\sin(f(x))\\cdot \\mathrm{D}f(x).$$$

Lean4

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

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