cmpLE_toDual

Mathlib.Order.Compare

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

English

In a context with orders, cmpLE on duals flips the order: cmpLE(toDual x)(toDual y) = cmpLE y x.

Русский

Для двойственного порядка cmpLE меняет направление: cmpLE(toDual x)(toDual y) = cmpLE y x.

LaTeX

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

Lean4

@[simp]
theorem cmpLE_toDual [LE α] [DecidableLE α] (x y : α) : cmpLE (toDual x) (toDual y) = cmpLE y x :=
  rfl

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

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

Разделы

Аффилиация

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