sinh_bijective

Mathlib.Analysis.SpecialFunctions.Arsinh

URI: https://scilib.ai/kg/mathlib#Real.sinh_bijective

English

Sinh on ℝ is a bijection with inverse arsinh.

Русский

Sinh на ℝ является биекцией с обратной функцией arsinh.

LaTeX

$$$\text{Bijective } \sinh_{\mathbb{R}}.$$$

Lean4

/-- `sinh` is bijective, both injective and surjective. -/
theorem sinh_bijective : Bijective sinh :=
  ⟨sinh_injective, sinh_surjective⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru