cmp_eq_gt

Mathlib.Order.Compare

URI: https://scilib.ai/kg/mathlib#LT.lt.cmp_eq_gt

English

In the LT.lt namespace, if x < y then cmp y x = Ordering.gt.

Русский

В области LT.lt при x < y выполняется cmp y x = Ordering.gt.

LaTeX

$$$\text{If } x < y, \text{ then } \mathrm{cmp}(y,x) = \mathrm{Ordering.gt}$$$

Lean4

theorem cmp_eq_gt (h : x < y) : cmp y x = Ordering.gt :=
  (cmp_eq_gt_iff _ _).2 h

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

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

Разделы

Аффилиация

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