Inverse of the sinh function
In this file we prove that sinh is bijective and hence has an inverse, arsinh.
Main Results
sinh_injective: The proof thatsinhis injectivesinh_surjective: The proof thatsinhis surjectivesinh_bijective: The proofsinhis bijectivearsinh: The inverse function ofsinh
Tags
arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective
sinh is injective, ∀ a b, sinh a = sinh b → a = b.
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.
arsinh is the left inverse of sinh.