cmp_eq

Mathlib.Order.Compare

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

English

If h is a Compares relation, then cmp a b equals o whenever o Compares a b.

Русский

Если h задаёт сопоставление сравнения, то cmp a b равно o тогда, когда o сопоставимо a и b.

LaTeX

$$$\\forall a\\ b\\ o,\\ o\\Compares a b \\rightarrow cmp a b = o$$$

Lean4

theorem cmp_eq [LinearOrder α] {a b : α} {o : Ordering} (h : o.Compares a b) : cmp a b = o :=
  (cmp_compares a b).inj h

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

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

Разделы

Аффилиация

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