sinhHomeomorph — Mathlib

English

The real hyperbolic sine function defines a homeomorphism of the real line onto itself; its inverse is arsinh, and both maps are continuous.

Русский

Гиперболический синус задаёт гомеоморфизм ℝ на ℝ; обратная функция — arsinh, обе отображения непрерывны.

LaTeX

$$$\\sinh: \\mathbb{R} \\to \\mathbb{R}$ is a bijection with inverse $\\operatorname{arsinh}$ and both maps are continuous;\\quad \\operatorname{arsinh} = \\sinh^{-1}.$$$

Lean4

/-- `Real.sinh` as a `Homeomorph`. -/
@[simps! -fullyApplied]
def sinhHomeomorph : ℝ ≃ₜ ℝ :=
  sinhOrderIso.toHomeomorph

Похожие утверждения