sin — Mathlib

English

If f has a derivative 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 : HasDerivAt f f' x) : HasDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') x :=
  (Real.hasDerivAt_sin (f x)).comp x hf

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