cmp_eq_lt

Mathlib.Order.Compare

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

English

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

Русский

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

LaTeX

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

Lean4

theorem cmp_eq_lt (h : x < y) : cmp x y = Ordering.lt :=
  (cmp_eq_lt_iff _ _).2 h

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

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

Разделы

Аффилиация

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