fderivWithin_ccosh — Mathlib

English

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

Русский

Если f дифференцируема внутри s в x и x является уникальной точкой внутри s, то fderivWithin косh(f) внутри s в x равняется sinh(f(x)) умноженному на fderivWithin f внутри s в x.

LaTeX

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

Lean4

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

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