Inverse of the sinh function #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that sinh is bijective and hence has an
Main definitions #
Main Results #
arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective
arsinh is defined using a logarithm,
arsinh x = log (x + sqrt(1 + x^2)).
arsinh is the right inverse of
sinh is surjective,
∀ b, ∃ a, sinh a = b. In this case, we use
a = arsinh b.
sinh is bijective, both injective and surjective.
arsinh is the left inverse of