ofDual_compares_ofDual — Mathlib

English

Similarly, for OrderDual, Compares o (ofDual a) (ofDual b) iff Compares o b a.

Русский

Аналогично, для OrderDual: Compares o (ofDual a) (ofDual b) ⇔ Compares o b a.

LaTeX

$$$\\forall o\\ {a b : α^{\\mathrm{op}}},\\ Compares o (ofDual a) (ofDual b) \\leftrightarrow Compares o b a$$$

Lean4

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

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