arsinh — Mathlib

English

If f has a derivative within s at a, then arsinh ∘ f has a derivative within s at a with the same factor.

Русский

Если у f в точке a внутри множества s существует производная, то arsinh ∘ f имеет такую же производную внутри s в a.

LaTeX

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

Lean4

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

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