fderiv_ccos — Mathlib

English

If f is differentiable at x, then fderiv of cos(f) at x equals −sin(f(x)) times fderiv at x.

Русский

Если f дифференцируема в x, то fderiv cos(f) в x равна −sin(f(x)) умножить на fderiv f в x.

LaTeX

$$$fderiv\\; (\\cos\\circ f)(x) = -\\sin(f(x))\\cdot fderiv\\; f(x).$$$

Lean4

@[simp]
theorem fderiv_ccos (hc : DifferentiableAt ℂ f x) :
    fderiv ℂ (fun x => Complex.cos (f x)) x = -Complex.sin (f x) • fderiv ℂ f x :=
  hc.hasFDerivAt.ccos.fderiv

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