Strict_Weak_Ordering_Induces_Partition
Provedorder-theoryproofwikirelation-theory
The incomparability relation of a strict weak ordering is an equivalence relation, inducing a partition.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Strict_Weak_Ordering_Induces_Partition {α : Type _} (R : α → α → Prop) (hIrrefl : ∀ x, ¬R x x) (hTrans : ∀ x y z, R x y → R y z → R x z) (hIncompTrans : ∀ x y z, (¬R x y ∧ ¬R y x) → (¬R y z ∧ ¬R z y) → (¬R x z ∧ ¬R z x)) : Equivalence (fun x y => ¬R x y ∧ ¬R y x) := by sorrySource