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 x y = Ordering.eq.

Русский

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

LaTeX

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

Lean4

theorem cmp_eq_eq (h : x = y) : cmp x y = Ordering.eq :=
  (cmp_eq_eq_iff _ _).2 h

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

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

Разделы

Аффилиация

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