sinh — Mathlib

English

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

Русский

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

LaTeX

$$HasFDerivWithinAt (fun x => Real.sinh (f x)) (Real.cosh (f x) • f') s x$$

Lean4

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

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