Complement_of_Strict_Total_Ordering
Provedorder-theoryproofwikirelation-theory
The complement of a strict total ordering is the union of the diagonal relation and the converse ordering.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Complement_of_Strict_Total_Ordering {α : Type _} (R : α → α → Prop) (hIrrefl : ∀ x, ¬R x x) (hTrans : ∀ x y z, R x y → R y z → R x z) (hTotal : ∀ x y, x ≠ y → R x y ∨ R y x) : ∀ x y, ¬R x y → (x = y ∨ R y x) := by sorrySource