# Documentation

Mathlib.Init.Order.Defs

# 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 , :
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a

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

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

The relation ≤ on a preorder is reflexive.

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

The relation ≤ on a preorder is transitive.

theorem lt_iff_le_not_le {α : Type u} [] {a : α} {b : α} :
a < b a b ¬b a
theorem lt_of_le_not_le {α : Type u} [] {a : α} {b : α} :
a b¬b aa < b
theorem le_not_le_of_lt {α : Type u} [] {a : α} {b : α} :
a < ba b ¬b a
theorem le_of_eq {α : Type u} [] {a : α} {b : α} :
a = ba b
theorem ge_trans {α : Type u} [] {a : α} {b : α} {c : α} :
a bb ca c
theorem lt_irrefl {α : Type u} [] (a : α) :
¬a < a
theorem gt_irrefl {α : Type u} [] (a : α) :
¬a > a
theorem lt_trans {α : Type u} [] {a : α} {b : α} {c : α} :
a < bb < ca < c
theorem gt_trans {α : Type u} [] {a : α} {b : α} {c : α} :
a > bb > ca > c
theorem ne_of_lt {α : Type u} [] {a : α} {b : α} (h : a < b) :
a b
theorem ne_of_gt {α : Type u} [] {a : α} {b : α} (h : b < a) :
a b
theorem lt_asymm {α : Type u} [] {a : α} {b : α} (h : a < b) :
¬b < a
theorem le_of_lt {α : Type u} [] {a : α} {b : α} :
a < ba b
theorem lt_of_lt_of_le {α : Type u} [] {a : α} {b : α} {c : α} :
a < bb ca < c
theorem lt_of_le_of_lt {α : Type u} [] {a : α} {b : α} {c : α} :
a bb < ca < c
theorem gt_of_gt_of_ge {α : Type u} [] {a : α} {b : α} {c : α} (h₁ : a > b) (h₂ : b c) :
a > c
theorem gt_of_ge_of_gt {α : Type u} [] {a : α} {b : α} {c : α} (h₁ : a b) (h₂ : b > c) :
a > c
instance instTransLeToLE {α : Type u} [] :
Trans LE.le LE.le LE.le
instance instTransLtToLT {α : Type u} [] :
Trans LT.lt LT.lt LT.lt
instance instTransLtToLTLeToLE {α : Type u} [] :
Trans LT.lt LE.le LT.lt
instance instTransLeToLELtToLT {α : Type u} [] :
Trans LE.le LT.lt LT.lt
instance instTransGeToLE {α : Type u} [] :
Trans GE.ge GE.ge GE.ge
instance instTransGtToLT {α : Type u} [] :
Trans GT.gt GT.gt GT.gt
instance instTransGtToLTGeToLE {α : Type u} [] :
Trans GT.gt GE.ge GT.gt
instance instTransGeToLEGtToLT {α : Type u} [] :
Trans GE.ge GT.gt GT.gt
theorem not_le_of_gt {α : Type u} [] {a : α} {b : α} (h : a > b) :
¬a b
theorem not_lt_of_ge {α : Type u} [] {a : α} {b : α} (h : a b) :
¬a < b
theorem le_of_lt_or_eq {α : Type u} [] {a : α} {b : α} :
a < b a = ba b
theorem le_of_eq_or_lt {α : Type u} [] {a : α} {b : α} (h : a = b a < b) :
a b
def decidableLTOfDecidableLE {α : Type u} [] [DecidableRel fun x x_1 => x x_1] :
DecidableRel fun x x_1 => x < x_1

< is decidable if ≤ is.

Instances For

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

class PartialOrder (α : Type u) extends :
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b

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

Instances
theorem le_antisymm {α : Type u} [] {a : α} {b : α} :
a bb aa = b
theorem le_antisymm_iff {α : Type u} [] {a : α} {b : α} :
a = b a b b a
theorem lt_of_le_of_ne {α : Type u} [] {a : α} {b : α} :
a ba ba < b
def decidableEqOfDecidableLE {α : Type u} [] [DecidableRel fun x x_1 => x x_1] :

Equality is decidable if ≤ is.

Instances For
theorem Decidable.lt_or_eq_of_le {α : Type u} [] [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} [] [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} [] [DecidableRel fun x x_1 => x x_1] {a : α} {b : α} :
a b a < b a = b
theorem lt_or_eq_of_le {α : Type u} [] {a : α} {b : α} :
a ba < b a = b
theorem le_iff_lt_or_eq {α : Type u} [] {a : α} {b : α} :
a b a < b a = b

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

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

Default definition of max.

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

Default definition of min.

Instances For

This attempts to prove that a given instance of compare is equal to compareOfLessAndEq by introducing the arguments and trying the following approaches in order:

1. seeing if rfl works
2. seeing if the compare at hand is nonetheless essentially compareOfLessAndEq, but, because of implicit arguments, requires us to unfold the defs and split the ifs in the definition of compareOfLessAndEq
3. seeing if we can split by cases on the arguments, then see if the defs work themselves out (useful when compare is defined via a match statement, as it is for Bool)
Instances For
class LinearOrder (α : Type u) extends , , , :
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a

A linear order is total.

• decidableLE : DecidableRel fun x x_1 => x x_1

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

• decidableEq :

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

• decidableLT : DecidableRel fun x x_1 => x < x_1

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

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

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} [] (a : α) (b : α) :
a b b a
theorem le_of_not_ge {α : Type u} [] {a : α} {b : α} :
¬a ba b
theorem le_of_not_le {α : Type u} [] {a : α} {b : α} :
¬a bb a
theorem not_lt_of_gt {α : Type u} [] {a : α} {b : α} (h : a > b) :
¬a < b
theorem lt_trichotomy {α : Type u} [] (a : α) (b : α) :
a < b a = b b < a
theorem le_of_not_lt {α : Type u} [] {a : α} {b : α} (h : ¬b < a) :
a b
theorem le_of_not_gt {α : Type u} [] {a : α} {b : α} :
¬a > ba b
theorem lt_of_not_ge {α : Type u} [] {a : α} {b : α} (h : ¬a b) :
a < b
theorem lt_or_le {α : Type u} [] (a : α) (b : α) :
a < b b a
theorem le_or_lt {α : Type u} [] (a : α) (b : α) :
a b b < a
theorem lt_or_ge {α : Type u} [] (a : α) (b : α) :
a < b a b
theorem le_or_gt {α : Type u} [] (a : α) (b : α) :
a b a > b
theorem lt_or_gt_of_ne {α : Type u} [] {a : α} {b : α} (h : a b) :
a < b a > b
theorem ne_iff_lt_or_gt {α : Type u} [] {a : α} {b : α} :
a b a < b a > b
theorem lt_iff_not_ge {α : Type u} [] (x : α) (y : α) :
x < y ¬x y
@[simp]
theorem not_lt {α : Type u} [] {a : α} {b : α} :
¬a < b b a
@[simp]
theorem not_le {α : Type u} [] {a : α} {b : α} :
¬a b b < a
instance instDecidableLtToLTToPreorderToPartialOrder {α : Type u} [] (a : α) (b : α) :
Decidable (a < b)
instance instDecidableLeToLEToPreorderToPartialOrder {α : Type u} [] (a : α) (b : α) :
instance instDecidableEq {α : Type u} [] (a : α) (b : α) :
Decidable (a = b)
theorem eq_or_lt_of_not_lt {α : Type u} [] {a : α} {b : α} (h : ¬a < b) :
a = b b < a
instance isStrictWeakOrder_of_linearOrder {α : Type u} [] :
IsStrictWeakOrder α fun x x_1 => x < x_1
instance isStrictTotalOrder_of_linearOrder {α : Type u} [] :
IsStrictTotalOrder α fun x x_1 => x < x_1
def ltByCases {α : Type u} [] (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.

Instances For
theorem le_imp_le_of_lt_imp_lt {α : Type u} {β : Type u_1} [] [] {a : α} {b : α} {c : β} {d : β} (H : d < cb < a) (h : a b) :
c d
theorem compare_lt_iff_lt {α : Type u} [] {a : α} {b : α} :
a < b
theorem compare_gt_iff_gt {α : Type u} [] {a : α} {b : α} :
a > b
theorem compare_eq_iff_eq {α : Type u} [] {a : α} {b : α} :
a = b
theorem compare_le_iff_le {α : Type u} [] {a : α} {b : α} :
a b
theorem compare_ge_iff_ge {α : Type u} [] {a : α} {b : α} :
a b
theorem compare_iff {α : Type u} [] (a : α) (b : α) {o : Ordering} :
compare a b = o
instance instTransCmpCompareToOrd {α : Type u} [] :
Std.TransCmp compare