arsinh — Mathlib

English

If f is differentiable at a, then arsinh ∘ f is differentiable at a.

Русский

Если функция f дифференцируема в точке a, то arsinh(f(x)) дифференцируема в точке a.

LaTeX

$$$\text{DifferentiableAt } f\ a \Rightarrow \text{DifferentiableAt } (x \mapsto \operatorname{arsinh}(f(x)))\ a$$$

Lean4

@[fun_prop]
theorem arsinh (h : DifferentiableAt ℝ f a) : DifferentiableAt ℝ (fun x => arsinh (f x)) a :=
  (differentiable_arsinh _).comp a h

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