fderiv_csin — Mathlib

English

If f is differentiable, then sin ∘ f is differentiable with derivative cos(f(x)) · f'(x).

Русский

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

LaTeX

$$$fderiv(\\sin\\circ f)(x) = \\cos(f(x)) \\cdot fderiv(f)(x).$$$

Lean4

@[simp]
theorem fderiv_csin (hc : DifferentiableAt ℂ f x) :
    fderiv ℂ (fun x => Complex.sin (f x)) x = Complex.cos (f x) • fderiv ℂ f x :=
  hc.hasFDerivAt.csin.fderiv

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