arsinh_le_arsinh

Mathlib.Analysis.SpecialFunctions.Arsinh

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

English

The order is preserved by arsinh: arsinh x ≤ arsinh y iff x ≤ y.

Русский

Порядок сохраняется под arsinh: arsinh x ≤ arsinh y ⇔ x ≤ y.

LaTeX

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

Lean4

@[simp]
theorem arsinh_le_arsinh : arsinh x ≤ arsinh y ↔ x ≤ y :=
  sinhOrderIso.symm.le_iff_le

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

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

Разделы

Аффилиация

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