hasStrictDerivAt_arsinh — Mathlib

English

The derivative of arsinh at x is 1/√(1+x^2).

Русский

Производная arsinh по x равна 1/√(1+x^2).

LaTeX

$$$\\frac{d}{dx}\\operatorname{arsinh}(x) = \\frac{1}{\\sqrt{1+x^2}}.$$$

Lean4

theorem hasStrictDerivAt_arsinh (x : ℝ) : HasStrictDerivAt arsinh (√(1 + x ^ 2))⁻¹ x :=
  by
  convert
    sinhHomeomorph.toOpenPartialHomeomorph.hasStrictDerivAt_symm (mem_univ x) (cosh_pos _).ne'
      (hasStrictDerivAt_sinh _) using
    2
  exact (cosh_arsinh _).symm

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