# Documentation

Mathlib.Init.Algebra.Order

# Orders #

Defines classes for preorders, partial orders, and linear orders and proves some basic lemmas about them.

### Definition of Preorder and lemmas about types with a Preorder#

class Preorder (α : Type u) extends , :

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

Instances
@[simp]
theorem le_refl {α : Type u} [inst : ] (a : α) :
a a

The relation ≤≤ on a preorder is reflexive.

theorem le_trans {α : Type u} [inst : ] {a : α} {b : α} {c : α} :
a bb ca c

The relation ≤≤ on a preorder is transitive.

theorem lt_iff_le_not_le {α : Type u} [inst : ] {a : α} {b : α} :
a < b a b ¬b a
theorem lt_of_le_not_le {α : Type u} [inst : ] {a : α} {b : α} :
a b¬b aa < b
theorem le_not_le_of_lt {α : Type u} [inst : ] {a : α} {b : α} :
a < ba b ¬b a
theorem le_of_eq {α : Type u} [inst : ] {a : α} {b : α} :
a = ba b
theorem ge_trans {α : Type u} [inst : ] {a : α} {b : α} {c : α} :
a bb ca c
theorem lt_irrefl {α : Type u} [inst : ] (a : α) :
¬a < a
theorem gt_irrefl {α : Type u} [inst : ] (a : α) :
¬a > a
theorem lt_trans {α : Type u} [inst : ] {a : α} {b : α} {c : α} :
a < bb < ca < c
theorem gt_trans {α : Type u} [inst : ] {a : α} {b : α} {c : α} :
a > bb > ca > c
theorem ne_of_lt {α : Type u} [inst : ] {a : α} {b : α} (h : a < b) :
a b
theorem ne_of_gt {α : Type u} [inst : ] {a : α} {b : α} (h : b < a) :
a b
theorem lt_asymm {α : Type u} [inst : ] {a : α} {b : α} (h : a < b) :
¬b < a
theorem le_of_lt {α : Type u} [inst : ] {a : α} {b : α} :
a < ba b
theorem lt_of_lt_of_le {α : Type u} [inst : ] {a : α} {b : α} {c : α} :
a < bb ca < c
theorem lt_of_le_of_lt {α : Type u} [inst : ] {a : α} {b : α} {c : α} :
a bb < ca < c
theorem gt_of_gt_of_ge {α : Type u} [inst : ] {a : α} {b : α} {c : α} (h₁ : a > b) (h₂ : b c) :
a > c
theorem gt_of_ge_of_gt {α : Type u} [inst : ] {a : α} {b : α} {c : α} (h₁ : a b) (h₂ : b > c) :
a > c
instance instTransLeToLE {α : Type u} [inst : ] :
Trans LE.le LE.le LE.le
Equations
• instTransLeToLE = { trans := (_ : ∀ {a b c : α}, a bb ca c) }
instance instTransLtToLT {α : Type u} [inst : ] :
Trans LT.lt LT.lt LT.lt
Equations
• instTransLtToLT = { trans := (_ : ∀ {a b c : α}, a < bb < ca < c) }
instance instTransLtToLTLeToLE {α : Type u} [inst : ] :
Trans LT.lt LE.le LT.lt
Equations
• instTransLtToLTLeToLE = { trans := (_ : ∀ {a b c : α}, a < bb ca < c) }
instance instTransLeToLELtToLT {α : Type u} [inst : ] :
Trans LE.le LT.lt LT.lt
Equations
• instTransLeToLELtToLT = { trans := (_ : ∀ {a b c : α}, a bb < ca < c) }
instance instTransGeToLE {α : Type u} [inst : ] :
Trans GE.ge GE.ge GE.ge
Equations
• instTransGeToLE = { trans := (_ : ∀ {a b c : α}, a bb ca c) }
instance instTransGtToLT {α : Type u} [inst : ] :
Trans GT.gt GT.gt GT.gt
Equations
• instTransGtToLT = { trans := (_ : ∀ {a b c : α}, a > bb > ca > c) }
instance instTransGtToLTGeToLE {α : Type u} [inst : ] :
Trans GT.gt GE.ge GT.gt
Equations
• instTransGtToLTGeToLE = { trans := (_ : ∀ {a b c : α}, a > bb ca > c) }
instance instTransGeToLEGtToLT {α : Type u} [inst : ] :
Trans GE.ge GT.gt GT.gt
Equations
• instTransGeToLEGtToLT = { trans := (_ : ∀ {a b c : α}, a bb > ca > c) }
theorem not_le_of_gt {α : Type u} [inst : ] {a : α} {b : α} (h : a > b) :
¬a b
theorem not_lt_of_ge {α : Type u} [inst : ] {a : α} {b : α} (h : a b) :
¬a < b
theorem le_of_lt_or_eq {α : Type u} [inst : ] {a : α} {b : α} :
a < b a = ba b
theorem le_of_eq_or_lt {α : Type u} [inst : ] {a : α} {b : α} (h : a = b a < b) :
a b
instance decidableLT_of_decidableLE {α : Type u} [inst : ] [inst : DecidableRel fun x x_1 => x x_1] :
DecidableRel fun x x_1 => x < x_1
Equations
• One or more equations did not get rendered due to their size.

### Definition of PartialOrder and lemmas about types with a partial order #

class PartialOrder (α : Type u) extends :
• le_antisymm : ∀ (a b : α), a bb aa = b

A partial order is a reflexive, transitive, antisymmetric relation ≤≤.

Instances
theorem le_antisymm {α : Type u} [inst : ] {a : α} {b : α} :
a bb aa = b
theorem le_antisymm_iff {α : Type u} [inst : ] {a : α} {b : α} :
a = b a b b a
theorem lt_of_le_of_ne {α : Type u} [inst : ] {a : α} {b : α} :
a ba ba < b
instance decidableEq_of_decidableLE {α : Type u} [inst : ] [inst : DecidableRel fun x x_1 => x x_1] :
Equations
theorem Decidable.lt_or_eq_of_le {α : Type u} [inst : ] [inst : DecidableRel fun x x_1 => x x_1] {a : α} {b : α} (hab : a b) :
a < b a = b
theorem Decidable.eq_or_lt_of_le {α : Type u} [inst : ] [inst : DecidableRel fun x x_1 => x x_1] {a : α} {b : α} (hab : a b) :
a = b a < b
theorem Decidable.le_iff_lt_or_eq {α : Type u} [inst : ] [inst : DecidableRel fun x x_1 => x x_1] {a : α} {b : α} :
a b a < b a = b
theorem lt_or_eq_of_le {α : Type u} [inst : ] {a : α} {b : α} :
a ba < b a = b
theorem le_iff_lt_or_eq {α : Type u} [inst : ] {a : α} {b : α} :
a b a < b a = b

### Definition of LinearOrder and lemmas about types with a linear order #

def maxDefault {α : Type u} [inst : LE α] [inst : DecidableRel fun x x_1 => x x_1] (a : α) (b : α) :
α

Default definition of max.

Equations
• = if a b then b else a
def minDefault {α : Type u} [inst : LE α] [inst : DecidableRel fun x x_1 => x x_1] (a : α) (b : α) :
α

Default definition of min.

Equations
• = if a b then a else b
class LinearOrder (α : Type u) extends , , :
• A linear order is total.

le_total : ∀ (a b : α), a b b a
• In a linearly ordered type, we assume the order relations are all decidable.

decidable_le : DecidableRel fun x x_1 => x x_1
• In a linearly ordered type, we assume the order relations are all decidable.

decidable_eq :
• In a linearly ordered type, we assume the order relations are all decidable.

decidable_lt : DecidableRel fun x x_1 => x < x_1
• The minimum function is equivalent to the one you get from minOfLe.

min_def : autoParam (∀ (a b : α), min a b = if a b then a else b) _auto✝
• The minimum function is equivalent to the one you get from maxOfLe.

max_def : autoParam (∀ (a b : α), max a b = if a b then b else a) _auto✝

A linear order is reflexive, transitive, antisymmetric and total relation ≤≤. We assume that every linear ordered type has decidable (≤)≤), (<), and (=).

Instances
theorem le_total {α : Type u} [inst : ] (a : α) (b : α) :
a b b a
theorem le_of_not_ge {α : Type u} [inst : ] {a : α} {b : α} :
¬a ba b
theorem le_of_not_le {α : Type u} [inst : ] {a : α} {b : α} :
¬a bb a
theorem not_lt_of_gt {α : Type u} [inst : ] {a : α} {b : α} (h : a > b) :
¬a < b
theorem lt_trichotomy {α : Type u} [inst : ] (a : α) (b : α) :
a < b a = b b < a
theorem le_of_not_lt {α : Type u} [inst : ] {a : α} {b : α} (h : ¬b < a) :
a b
theorem le_of_not_gt {α : Type u} [inst : ] {a : α} {b : α} :
¬a > ba b
theorem lt_of_not_ge {α : Type u} [inst : ] {a : α} {b : α} (h : ¬a b) :
a < b
theorem lt_or_le {α : Type u} [inst : ] (a : α) (b : α) :
a < b b a
theorem le_or_lt {α : Type u} [inst : ] (a : α) (b : α) :
a b b < a
theorem lt_or_ge {α : Type u} [inst : ] (a : α) (b : α) :
a < b a b
theorem le_or_gt {α : Type u} [inst : ] (a : α) (b : α) :
a b a > b
theorem lt_or_gt_of_ne {α : Type u} [inst : ] {a : α} {b : α} (h : a b) :
a < b a > b
theorem ne_iff_lt_or_gt {α : Type u} [inst : ] {a : α} {b : α} :
a b a < b a > b
theorem lt_iff_not_ge {α : Type u} [inst : ] (x : α) (y : α) :
x < y ¬x y
@[simp]
theorem not_lt {α : Type u} [inst : ] {a : α} {b : α} :
¬a < b b a
@[simp]
theorem not_le {α : Type u} [inst : ] {a : α} {b : α} :
¬a b b < a
instance instDecidableLtToLTToPreorderToPartialOrder {α : Type u} [inst : ] (a : α) (b : α) :
Decidable (a < b)
Equations
instance instDecidableLeToLEToPreorderToPartialOrder {α : Type u} [inst : ] (a : α) (b : α) :
Equations
instance instDecidableEq {α : Type u} [inst : ] (a : α) (b : α) :
Decidable (a = b)
Equations
theorem eq_or_lt_of_not_lt {α : Type u} [inst : ] {a : α} {b : α} (h : ¬a < b) :
a = b b < a
def lt_by_cases {α : Type u} [inst : ] (x : α) (y : α) {P : Sort u_1} (h₁ : x < yP) (h₂ : x = yP) (h₃ : y < xP) :
P

Perform a case-split on the ordering of x and y in a decidable linear order.

Equations
• lt_by_cases x y h₁ h₂ h₃ = if h : x < y then h₁ h else if h' : y < x then h₃ h' else h₂ (_ : x = y)
theorem le_imp_le_of_lt_imp_lt {α : Type u} {β : Type u_1} [inst : ] [inst : ] {a : α} {b : α} {c : β} {d : β} (H : d < cb < a) (h : a b) :
c d