sin — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sin (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') s x :=
  (Real.hasDerivAt_sin (f x)).comp_hasDerivWithinAt x hf

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