cmp_toDual

Mathlib.Order.Compare

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

English

Under LT and decidable LT, cmp(toDual x)(toDual y) equals cmp y x.

Русский

При наличии LT и решаемого LT, cmp(toDual x)(toDual y) равно cmp y x.

LaTeX

$$$\\forall x\\ y,\\ cmp (toDual x) (toDual y) = cmp y x$$$

Lean4

@[simp]
theorem cmp_toDual [LT α] [DecidableLT α] (x y : α) : cmp (toDual x) (toDual y) = cmp y x :=
  rfl

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

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

Разделы

Аффилиация

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