mathlib documentation

analysis.special_functions.arsinh

Inverse of the sinh function

In this file we prove that sinh is bijective and hence has an inverse, arsinh.

Main Results

Tags

arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective

def real.arsinh  :

arsinh is defined using a logarithm, arsinh x = log (x + sqrt(1 + x^2)).

Equations

sinh is injective, ∀ a b, sinh a = sinh b → a = b.

theorem real.sinh_arsinh (x : ) :

arsinh is the right inverse of sinh.

sinh is surjective, ∀ b, ∃ a, sinh a = b. In this case, we use a = arsinh b.

sinh is bijective, both injective and surjective.

A rearrangement and sqrt of real.cosh_sq_sub_sinh_sq.

theorem real.arsinh_sinh (x : ) :

arsinh is the left inverse of sinh.