English
Let sinh: R → R be the hyperbolic sine function. It is an order-preserving bijection from R to R, hence it defines an order isomorphism of the real line with itself. Consequently, its inverse arsinh is also order-preserving and bijective.
Русский
Пусть sinh: ℝ → ℝ — гиперболический синус. Это отображение, сохраняющее порядок, и биекция на ℝ, следовательно, образует порядковый изоморфизм ℝ с самой собой; обратная функция arsinh также биективна и монотонна.
LaTeX
$$$\\left( \\forall x,y \\in \\mathbb{R},\\ x \\le y \\iff \\sinh x \\le \\sinh y \\right) \\land \\left( \\forall t \\in \\mathbb{R},\\ \\operatorname{arsinh}(\\sinh t) = t \\land \\sinh(\\operatorname{arsinh} t) = t \\right).$$$
Lean4
/-- `Real.sinh` as an `OrderIso`. -/
@[simps! -fullyApplied]
def sinhOrderIso : ℝ ≃o ℝ where
toEquiv := sinhEquiv
map_rel_iff' := @sinh_le_sinh
