derivWithin_csin — Mathlib

English

Within a set, the derivative of sinh(f(x)) equals cosh(f(x)) times derivWithin f.

Русский

Внутри множества производная sinh(f(x)) равна cosh(f(x))·derivWithin f.

LaTeX

$$$\operatorname{derivWithin}(\sinh(f(z)), s, x) = \cosh(f(x)) \cdot \operatorname{derivWithin}(f, s, x).$$$

Lean4

theorem derivWithin_csin (hf : DifferentiableWithinAt ℂ f s x) (hxs : UniqueDiffWithinAt ℂ s x) :
    derivWithin (fun x => Complex.sin (f x)) s x = Complex.cos (f x) * derivWithin f s x :=
  hf.hasDerivWithinAt.csin.derivWithin hxs

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