fderivWithin_ccos — Mathlib

English

If f is differentiable within s at x, then the derivative within s of cos(f(x)) is −sin(f(x)) times the derivative within s of f.

Русский

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

LaTeX

$$$\\mathrm{fderivWithin} \\; (\\cos\\circ f)\\; s\\; x = -\\sin(f(x))\\cdot \\mathrm{fderivWithin}\\; f\\; s\\; x.$$$

Lean4

theorem fderivWithin_ccos (hf : DifferentiableWithinAt ℂ f s x) (hxs : UniqueDiffWithinAt ℂ s x) :
    fderivWithin ℂ (fun x => Complex.cos (f x)) s x = -Complex.sin (f x) • fderivWithin ℂ f s x :=
  hf.hasFDerivWithinAt.ccos.fderivWithin hxs

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