derivWithin_cos — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{derivWithin}(\\cos \\circ f)\\ s\\ x = -\\sin(f(x)) \\cdot \\text{derivWithin}(f)\\ s\\ x$$$

Lean4

theorem derivWithin_cos (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
    derivWithin (fun x => Real.cos (f x)) s x = -Real.sin (f x) * derivWithin f s x :=
  hf.hasDerivWithinAt.cos.derivWithin hxs

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