cmp_eq_gt_iff

Mathlib.Order.Compare

URI: https://scilib.ai/kg/mathlib#cmp_eq_gt_iff

English

For a LinearOrder α, cmp x y = Ordering.gt if and only if y < x.

Русский

Для линейного порядка α cmp x y = Ordering.gt тогда и только тогда, когда y < x.

LaTeX

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

Lean4

@[simp]
theorem cmp_eq_gt_iff : cmp x y = Ordering.gt ↔ y < x :=
  Ordering.Compares.eq_gt (cmp_compares x y)

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

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

Разделы

Аффилиация

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