ccosh — Mathlib

English

Let f: E → ℂ be differentiable at x with derivative f'. Then the derivative of the composite x ↦ cosh(f(x)) at x is sinh(f(x)) times f'.

Русский

Пусть f: E → ℂ дифференцируема в точке x с производной f'. Тогда производная композиции x ↦ cosh(f(x)) в точке x равна sinh(f(x)) умножению на f'.

LaTeX

$$$$ D(\cosh \circ f)(x) = \sinh(f(x)) \cdot Df(x). $$$$

Lean4

theorem ccosh (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) • f') x :=
  (Complex.hasDerivAt_cosh (f x)).comp_hasFDerivAt x hf

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