mathlib documentation


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

noncomputable def real.arsinh (x : ) :

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.