arsinh — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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