derivWithin_ccosh — Mathlib

English

Within a set, the derivative of cosh(f(x)) obeys the same chain rule in the derivWithin sense.

Русский

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

LaTeX

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

Lean4

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

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