derivWithin_ccos — Mathlib

English

Within a set, the derivative of cos(f(x)) behaves by the same chain rule.

Русский

Внутри множества производная cos(f(x)) следует тому же цепному правилу.

LaTeX

$$$\operatorname{derivWithin}(\cos(f(z)), s, x) = -\sin(f(x)) \cdot \operatorname{derivWithin}(f, s, x).$$$

Lean4

theorem derivWithin_ccos (hf : DifferentiableWithinAt ℂ f s x) (hxs : UniqueDiffWithinAt ℂ s x) :
    derivWithin (fun x => Complex.cos (f x)) s x = -Complex.sin (f x) * derivWithin f s x :=
  hf.hasDerivWithinAt.ccos.derivWithin hxs

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