class Lean.Grind.Preorder (α : Type u) extends LE α, LT α : Type u

A preorder is a reflexive, transitive relation ≤ with a < b defined in the obvious way.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans {a b c : α} : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le {a b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem Lean.Grind.Preorder.le_of_lt {α : Type u} [Preorder α] {a b : α} (h : a < b) : a ≤ b

theorem Lean.Grind.Preorder.lt_of_lt_of_le {α : Type u} [Preorder α] {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) : a < c

theorem Lean.Grind.Preorder.lt_of_le_of_lt {α : Type u} [Preorder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : a < c

theorem Lean.Grind.Preorder.lt_trans {α : Type u} [Preorder α] {a b c : α} (h₁ : a < b) (h₂ : b < c) : a < c

theorem Lean.Grind.Preorder.lt_irrefl {α : Type u} [Preorder α] (a : α) : ¬a < a

theorem Lean.Grind.Preorder.ne_of_lt {α : Type u} [Preorder α] {a b : α} (h : a < b) : a ≠ b

theorem Lean.Grind.Preorder.ne_of_gt {α : Type u} [Preorder α] {a b : α} (h : a > b) : a ≠ b

theorem Lean.Grind.Preorder.not_ge_of_lt {α : Type u} [Preorder α] {a b : α} (h : a < b) : ¬b ≤ a

theorem Lean.Grind.Preorder.not_gt_of_lt {α : Type u} [Preorder α] {a b : α} (h : a < b) : ¬a > b

class Lean.Grind.PartialOrder (α : Type u) extends Lean.Grind.Preorder α : Type u

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans {a b c : α} : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le {a b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm {a b : α} : a ≤ b → b ≤ a → a = b

theorem Lean.Grind.PartialOrder.le_iff_lt_or_eq {α : Type u} [PartialOrder α] {a b : α} : a ≤ b ↔ a < b ∨ a = b

class Lean.Grind.LinearOrder (α : Type u) extends Lean.Grind.PartialOrder α : Type u

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans {a b c : α} : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le {a b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm {a b : α} : a ≤ b → b ≤ a → a = b
• le_total (a b : α) : a ≤ b ∨ b ≤ a

theorem Lean.Grind.LinearOrder.trichotomy {α : Type u} [LinearOrder α] (a b : α) : a < b ∨ a = b ∨ b < a