cmp_eq_eq_iff

Mathlib.Order.Compare

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

English

In a LinearOrder α, if x = y then cmp x y = Ordering.eq.

Русский

В линейном порядке α если x = y, тогда cmp x y = Ordering.eq.

LaTeX

$$$x = y \Rightarrow \mathrm{cmp}(x,y) = \mathrm{Ordering.eq}$$$

Lean4

@[simp]
theorem cmp_eq_eq_iff : cmp x y = Ordering.eq ↔ x = y :=
  Ordering.Compares.eq_eq (cmp_compares x y)

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

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

Разделы

Аффилиация

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