class Lean.Grind.Preorder (α : Type u) [LE α] [LT α] : Prop

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

• le_refl (a : α) : a ≤ a

  The less-than-or-equal relation is reflexive.

• le_trans {a b c : α} : a ≤ b → b ≤ c → a ≤ c

  The less-than-or-equal relation is transitive.

• lt_iff_le_not_le {a b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a

  The less-than relation is determined by the less-than-or-equal relation.

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

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

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

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

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

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

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

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

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

class Lean.Grind.PartialOrder (α : Type u) [LE α] [LT α] extends Lean.Grind.Preorder α : Prop

A partial order is a preorder with the additional property that a ≤ b and b ≤ a implies a = b.

• 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

  The less-than-or-equal relation is antisymmetric.

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

class Lean.Grind.LinearOrder (α : Type u) [LE α] [LT α] extends Lean.Grind.PartialOrder α : Prop

A linear order is a partial order with the additional property that every pair of elements is comparable.

• 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

  For every two elements a and b, either a ≤ b or b ≤ a.

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

theorem Lean.Grind.LinearOrder.le_of_not_lt {α : Type u} [LE α] [LT α] [LinearOrder α] {a b : α} (h : ¬a < b) : b ≤ a

theorem Lean.Grind.LinearOrder.lt_of_not_le {α : Type u} [LE α] [LT α] [LinearOrder α] {a b : α} (h : ¬a ≤ b) : b < a