derivWithin_sin — Mathlib

English

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

Русский

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

LaTeX

$$$\\frac{d}{dx}\\bigl(\\sin(f(x))\\bigr) = \\cos(f(x)) \\cdot f'(x).$$$

Lean4

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

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