derivWithin_csinh — Mathlib

English

Within a set, the derivative of sinh(f(x)) follows the same derivWithin rule.

Русский

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

LaTeX

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

Lean4

theorem derivWithin_csinh (hf : DifferentiableWithinAt ℂ f s x) (hxs : UniqueDiffWithinAt ℂ s x) :
    derivWithin (fun x => Complex.sinh (f x)) s x = Complex.cosh (f x) * derivWithin f s x :=
  hf.hasDerivWithinAt.csinh.derivWithin hxs

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