# mathlibdocumentation

core.init.algebra.order

@[instance]
def preorder.to_has_lt (α : Type u) [s : preorder α] :

@[class]
structure preorder  :
Type uType u
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"

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

Instances
@[instance]
def preorder.to_has_le (α : Type u) [s : preorder α] :

@[class]
structure partial_order  :
Type uType u
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b

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

Instances
@[instance]
def partial_order.to_preorder (α : Type u) [s : partial_order α] :

@[class]
structure linear_order  :
Type uType u
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_total : ∀ (a b : α), a b b a

A linear order is reflexive, transitive, antisymmetric and total relation ≤.

Instances
@[instance]
def linear_order.to_partial_order (α : Type u) [s : linear_order α] :

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

The relation ≤ on a preorder is reflexive.

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

The relation ≤ on a preorder is transitive.

theorem lt_iff_le_not_le {α : Type u} [preorder α] {a b : α} :
a < b a b ¬b a

theorem lt_of_le_not_le {α : Type u} [preorder α] {a b : α} :
a b¬b aa < b

theorem le_not_le_of_lt {α : Type u} [preorder α] {a b : α} :
a < ba b ¬b a

theorem le_antisymm {α : Type u} {a b : α} :
a bb aa = b

theorem le_of_eq {α : Type u} [preorder α] {a b : α} :
a = ba b

theorem le_antisymm_iff {α : Type u} {a b : α} :
a = b a b b a

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

theorem le_total {α : Type u} [linear_order α] (a b : α) :
a b b a

theorem le_of_not_ge {α : Type u} [linear_order α] {a b : α} :
¬a ba b

theorem le_of_not_le {α : Type u} [linear_order α] {a b : α} :
¬a bb a

theorem lt_irrefl {α : Type u} [preorder α] (a : α) :
¬a < a

theorem gt_irrefl {α : Type u} [preorder α] (a : α) :
¬a > a

theorem lt_trans {α : Type u} [preorder α] {a b c : α} :
a < bb < ca < c

def lt.trans {α : Type u_1} [preorder α] {a b c : α} :
a < bb < ca < c

theorem gt_trans {α : Type u} [preorder α] {a b c : α} :
a > bb > ca > c

def gt.trans {α : Type u_1} [preorder α] {a b c : α} :
a > bb > ca > c

theorem ne_of_lt {α : Type u} [preorder α] {a b : α} :
a < ba b

theorem ne_of_gt {α : Type u} [preorder α] {a b : α} :
a > ba b

theorem lt_asymm {α : Type u} [preorder α] {a b : α} :
a < b¬b < a

theorem not_lt_of_gt {α : Type u} [linear_order α] {a b : α} :
a > b¬a < b

theorem le_of_lt {α : Type u} [preorder α] {a b : α} :
a < ba b

theorem lt_of_lt_of_le {α : Type u} [preorder α] {a b c : α} :
a < bb ca < c

theorem lt_of_le_of_lt {α : Type u} [preorder α] {a b c : α} :
a bb < ca < c

theorem gt_of_gt_of_ge {α : Type u} [preorder α] {a b c : α} :
a > bb ca > c

theorem gt_of_ge_of_gt {α : Type u} [preorder α] {a b c : α} :
a bb > ca > c

theorem not_le_of_gt {α : Type u} [preorder α] {a b : α} :
a > b¬a b

theorem not_lt_of_ge {α : Type u} [preorder α] {a b : α} :
a b¬a < b

theorem lt_or_eq_of_le {α : Type u} {a b : α} :
a ba < b a = b

theorem le_of_lt_or_eq {α : Type u} [preorder α] {a b : α} :
a < b a = ba b

theorem le_iff_lt_or_eq {α : Type u} {a b : α} :
a b a < b a = b

theorem lt_of_le_of_ne {α : Type u} {a b : α} :
a ba ba < b

theorem lt_trichotomy {α : Type u} [linear_order α] (a b : α) :
a < b a = b b < a

theorem le_of_not_gt {α : Type u} [linear_order α] {a b : α} :
¬a > ba b

theorem lt_of_not_ge {α : Type u} [linear_order α] {a b : α} :
¬a ba < b

theorem lt_or_ge {α : Type u} [linear_order α] (a b : α) :
a < b a b

theorem le_or_gt {α : Type u} [linear_order α] (a b : α) :
a b a > b

theorem lt_or_gt_of_ne {α : Type u} [linear_order α] {a b : α} :
a ba < b a > b

theorem le_of_eq_or_lt {α : Type u} [preorder α] {a b : α} :
a = b a < ba b

theorem ne_iff_lt_or_gt {α : Type u} [linear_order α] {a b : α} :
a b a < b a > b

theorem lt_iff_not_ge {α : Type u} [linear_order α] (x y : α) :
x < y ¬x y

@[simp]
theorem not_lt {α : Type u} [linear_order α] {a b : α} :
¬a < b b a

@[simp]
theorem not_le {α : Type u} [linear_order α] {a b : α} :
¬a b b < a

@[instance]
def decidable_lt_of_decidable_le {α : Type u} [preorder α]  :

Equations
@[instance]
def decidable_eq_of_decidable_le {α : Type u}  :

Equations
@[class]
structure decidable_linear_order  :
Type uType u
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :

Instances
@[instance]

@[instance]
def has_lt.lt.decidable {α : Type u} (a b : α) :
decidable (a < b)

Equations
@[instance]
def has_le.le.decidable {α : Type u} (a b : α) :

Equations
@[instance]
def eq.decidable {α : Type u} (a b : α) :
decidable (a = b)

Equations
theorem eq_or_lt_of_not_lt {α : Type u} {a b : α} :
¬a < ba = b b < a

@[instance]
def has_le.le.is_total_preorder {α : Type u}  :

@[instance]

@[instance]

theorem decidable.lt_or_eq_of_le {α : Type u} {a b : α} :
a ba < b a = b

theorem decidable.eq_or_lt_of_le {α : Type u} {a b : α} :
a ba = b a < b

theorem decidable.le_iff_lt_or_eq {α : Type u} {a b : α} :
a b a < b a = b

theorem decidable.le_of_not_lt {α : Type u} {a b : α} :
¬b < aa b

theorem decidable.not_lt {α : Type u} {a b : α} :
¬a < b b a

theorem decidable.lt_or_le {α : Type u} (a b : α) :
a < b b a

theorem decidable.le_or_lt {α : Type u} (a b : α) :
a b b < a

theorem decidable.lt_trichotomy {α : Type u} (a b : α) :
a < b a = b b < a

theorem decidable.lt_or_gt_of_ne {α : Type u} {a b : α} :
a ba < b b < a

def decidable.lt_by_cases {α : Type u} (x y : α) {P : Sort u_1} :
(x < y → P)(x = y → P)(y < x → P) → P

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

Equations
• h₁ h₂ h₃ = dite (x < y) (λ (h : x < y), h₁ h) (λ (h : ¬x < y), dite (y < x) (λ (h' : y < x), h₃ h') (λ (h' : ¬y < x), h₂ _))
theorem decidable.ne_iff_lt_or_gt {α : Type u} {a b : α} :
a b a < b b < a

theorem decidable.le_imp_le_of_lt_imp_lt {α : Type u} {β : Type u_1} [preorder α] {a b : α} {c d : β} :
(d < cb < a)a bc d