mathlib documentation


Inverse of the sinh function

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

Main Results


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)).


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.