cmp_eq_eq'

Mathlib.Order.Compare

URI: https://scilib.ai/kg/mathlib#Eq.cmp_eq_eq'

English

In namespace Eq, if x = y then cmp y x = Ordering.eq.

Русский

В пространстве Eq, если x = y тогда cmp y x = Ordering.eq.

LaTeX

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

Lean4

theorem cmp_eq_eq' (h : x = y) : cmp y x = Ordering.eq :=
  h.symm.cmp_eq_eq

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

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

Разделы

Аффилиация

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