ne_gt

Mathlib.Order.Compare

URI: https://scilib.ai/kg/mathlib#Ordering.Compares.ne_gt

English

If o and a,b satisfy Compares o a b, then o ≠ gt iff a ≤ b.

Русский

Если o сравнивает a и b, то o ≠ gt тогда и только тогда, когда a ≤ b.

LaTeX

$$$\\forall o\\ {a}{b},\\ Compares o a b \\rightarrow (o \\neq gt \\leftrightarrow a \\le b)$$$

Lean4

theorem ne_gt [Preorder α] {o} {a b : α} (h : Compares o a b) : o ≠ gt ↔ a ≤ b :=
  (not_congr swap_eq_iff_eq_swap.symm).trans h.swap.ne_lt

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

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

Разделы

Аффилиация

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