arsinh_inj

Mathlib.Analysis.SpecialFunctions.Arsinh

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

English

For all real x,y, arsinh x = arsinh y implies x = y.

Русский

Для всех x,y ∈ ℝ, arsinh x = arsinh y ⇒ x = y.

LaTeX

$$$\\forall x,y \\in \\mathbb{R},\\ \\operatorname{arsinh} x = \\operatorname{arsinh} y \\iff x = y.$$$

Lean4

@[simp]
theorem arsinh_inj : arsinh x = arsinh y ↔ x = y :=
  arsinh_injective.eq_iff

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

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

Разделы

Аффилиация

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