fderivWithin_csinh — Mathlib

English

If f is differentiableWithinAt s x, then fderivWithin of sinh(f) within s at x equals cosh(f(x)) times fderivWithin of f within s at x.

Русский

Если f дифференцируема внутри s в x, то fderivWithin(sinh ∘ f) внутри s в x равна cosh(f(x)) умножить на fderivWithin f внутри s в x.

LaTeX

$$$$ fderivWithin_{\mathbb{C}}(\sinh \circ f)\; s\; x = \cosh(f(x)) \cdot fderivWithin_{\mathbb{C}} f\; s\; x. $$$$

Lean4

theorem fderivWithin_csinh (hf : DifferentiableWithinAt ℂ f s x) (hxs : UniqueDiffWithinAt ℂ s x) :
    fderivWithin ℂ (fun x => Complex.sinh (f x)) s x = Complex.cosh (f x) • fderivWithin ℂ f s x :=
  hf.hasFDerivWithinAt.csinh.fderivWithin hxs

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