Trichotomy_Law_Ordering
Provednamed-theoremsproofwikitotal-orderingstrichotomies
Let (S, ≤) be a totally ordered set. For all a, b in S, exactly one of the following holds: a < b, a = b, or b < a.
Preamble
import Mathlib.Order.Basic
Formal statement
theorem Trichotomy_Law_Ordering {α : Type _} [LinearOrder α] (a b : α) : a < b ∨ a = b ∨ b < a := by sorrySource