arsinh — Mathlib

English

If f has derivative f' at a, then arsinh ∘ f has derivative ((√(1+f(a)^2))^{-1}) • f' at a.

Русский

Если у f в точке a есть производная f', то arsinh ∘ f имеет производную ((√(1+f(a)^2))^{-1}) • f' в a.

LaTeX

$$$\text{HasDerivAt } f\ f'\ a \Rightarrow \text{HasDerivAt } (x \mapsto \operatorname{arsinh}(f(x)))\ ((\sqrt{1 + f(a)^2})^{-1} \cdot f')\ a$$$

Lean4

theorem arsinh (hf : HasDerivAt f f' a) : HasDerivAt (fun x => arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a :=
  (hasDerivAt_arsinh _).comp a hf

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