exp_arsinh

Mathlib.Analysis.SpecialFunctions.Arsinh

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

English

The exponential of arsinh x equals x plus the square root of (1+x^2): exp(arsinh x) = x + sqrt(1+x^2).

Русский

Экспонента arsinh x равна x плюс корень из (1+x^2): exp(arsinh x) = x + sqrt(1+x^2).

LaTeX

$$$\exp(\operatorname{arsinh} x) = x + \sqrt{1 + x^2}.$$$

Lean4

theorem exp_arsinh (x : ℝ) : exp (arsinh x) = x + √(1 + x ^ 2) :=
  by
  apply exp_log
  rw [← neg_lt_iff_pos_add']
  apply lt_sqrt_of_sq_lt
  simp

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

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

Разделы

Аффилиация

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