fderiv_sin — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{fderiv }(\\sin(f))(x) = \\cos(f(x)) \\cdot f'(x)$$$

Lean4

@[simp]
theorem fderiv_sin (hc : DifferentiableAt ℝ f x) :
    fderiv ℝ (fun x => Real.sin (f x)) x = Real.cos (f x) • fderiv ℝ f x :=
  hc.hasFDerivAt.sin.fderiv

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