fderivWithin_sin — Mathlib

English

If hf differentiableWithinAt f s x, then fderivWithin of sin(f) within s at x equals cos(f(x)) times fderivWithin f s x.

Русский

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

LaTeX

$$$\\text{fderivWithin }\\mathbb{R}(\\sin(f(x))) s x = \\cos(f(x)) \\cdot \\text{fderivWithin }\\mathbb{R} f s x$$$

Lean4

theorem fderivWithin_sin (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
    fderivWithin ℝ (fun x => Real.sin (f x)) s x = Real.cos (f x) • fderivWithin ℝ f s x :=
  hf.hasFDerivWithinAt.sin.fderivWithin hxs

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