arsinh_bijective

Mathlib.Analysis.SpecialFunctions.Arsinh

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

English

The function arsinh is a bijection from R to R; it is a two-sided inverse to sinh.

Русский

Функция arsinh является биекцией от ℝ к ℝ; она двусторонний обратный к sinh.

LaTeX

$$$\\operatorname{Bijective}(\\operatorname{arsinh}).$$$

Lean4

theorem arsinh_bijective : Bijective arsinh :=
  sinhEquiv.symm.bijective

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

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

Разделы

Аффилиация

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