cosh — Mathlib

English

If HasFDerivWithinAt f f' s x, then HasFDerivWithinAt (cosh(f x)) (sinh(f x) • f') s x.

Русский

Если у f в точке x внутри области s есть производная f', то производная cosh(f(x)) внутри s равна sinh(f(x)) · f'.

LaTeX

$$HasFDerivWithinAt (cosh ∘ f) (sinh (f x) • f') s x$$

Lean4

theorem cosh (hf : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (fun x => Real.cosh (f x)) (Real.sinh (f x) • f') s x :=
  (Real.hasDerivAt_cosh (f x)).comp_hasFDerivWithinAt x hf

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