fderivWithin_cos — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{fderivWithin }\\mathbb{R} (\\cos(f(x)))\\ s\\ x = -\\sin(f(x)) \\cdot \\text{fderivWithin }\\mathbb{R} f s x$$$

Lean4

theorem fderivWithin_cos (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
    fderivWithin ℝ (fun x => Real.cos (f x)) s x = -Real.sin (f x) • fderivWithin ℝ f s x :=
  hf.hasFDerivWithinAt.cos.fderivWithin hxs

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