toDual_compares_toDual — Mathlib

English

Under LT, comparing toDual flips the order: Compares o (toDual a) (toDual b) iff Compares o b a.

Русский

В линейном порядке, сопоставляя через toDual, порядок разворачивается: Compares o (toDual a) (toDual b) эквивалентно Compares o b a.

LaTeX

$$$\\forall o\\ a\\ b,\\ Compares o (toDual a) (toDual b) \\leftrightarrow Compares o b a$$$

Lean4

@[simp]
theorem toDual_compares_toDual [LT α] {a b : α} {o : Ordering} : Compares o (toDual a) (toDual b) ↔ Compares o b a :=
  by
  cases o
  exacts [Iff.rfl, eq_comm, Iff.rfl]

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