arsinh_nonneg_iff

Mathlib.Analysis.SpecialFunctions.Arsinh

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

English

0 ≤ arsinh x iff 0 ≤ x.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem arsinh_nonneg_iff : 0 ≤ arsinh x ↔ 0 ≤ x := by rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]

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

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

Разделы

Аффилиация

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