arsinh_pos_iff

Mathlib.Analysis.SpecialFunctions.Arsinh

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

English

0 < arsinh x iff 0 < x.

Русский

0 < arsinh x тогда и только тогда, когда 0 < x.

LaTeX

$$$0 < \\operatorname{arsinh} x \\iff 0 < x.$$$

Lean4

@[simp]
theorem arsinh_pos_iff : 0 < arsinh x ↔ 0 < x :=
  lt_iff_lt_of_le_iff_le arsinh_nonpos_iff

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

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

Разделы

Аффилиация

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