derivWithin_cosh — Mathlib

English

If f is differentiable within s at x and the derivative is well-defined, then the derivative within s of cosh(f(x)) equals sinh(f(x)) times the derivative within s of f.

Русский

Если f дифференцируема внутри s в точке x и производная существует, то производная cosh(f(x)) внутри s равна sinh(f(x)) умножить на производную внутри s от f.

LaTeX

$$$\\text{derivWithin}(\\cosh \\circ f)\\ s\\ x = \\sinh(f(x)) \\cdot \\text{derivWithin}(f\\ s)\\ x$$$

Lean4

theorem derivWithin_cosh (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
    derivWithin (fun x => Real.cosh (f x)) s x = Real.sinh (f x) * derivWithin f s x :=
  hf.hasDerivWithinAt.cosh.derivWithin hxs

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