fderivWithin_csin — Mathlib

English

If f has a derivative within s at x, then the derivative within s of sin(f(x)) is cos(f(x)) · f'.

Русский

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

LaTeX

$$$fderivWithin(\\sin\\circ f)(s,x) = \\cos(f(x)) \\cdot fderivWithin(f)(s,x).$$$

Lean4

theorem fderivWithin_csin (hf : DifferentiableWithinAt ℂ f s x) (hxs : UniqueDiffWithinAt ℂ s x) :
    fderivWithin ℂ (fun x => Complex.sin (f x)) s x = Complex.cos (f x) • fderivWithin ℂ f s x :=
  hf.hasFDerivWithinAt.csin.fderivWithin hxs

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