# Orders #

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

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

source
def maxDefault {α : Type u_1} [LE α] [DecidableLE α] (a b : α) :
α

Default definition of `max`.

Equations

- maxDefault a b = if a ≤ b then b else a

Instances For

source
def minDefault {α : Type u_1} [LE α] [DecidableLE α] (a b : α) :
α

Default definition of `min`.

Equations

- minDefault a b = if a ≤ b then a else b

Instances For

source
def tacticCompareOfLessAndEq_rfl :
Lean.ParserDescr

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 `if`s 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`)

Equations

- tacticCompareOfLessAndEq_rfl = Lean.ParserDescr.node `tacticCompareOfLessAndEq_rfl 1024 (Lean.ParserDescr.nonReservedSymbol "compareOfLessAndEq_rfl" false)

Instances For

source
class LinearOrder (α : Type u_2) extends PartialOrder α, Min α, Max α, Ord α :
Type u_2

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

- le : α → α → Prop
- lt : α → α → Prop
- le_refl (a : α) : a ≤ a
- le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
- le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
- min : α → α → α
- max : α → α → α
- compare : α → α → Ordering
- le_total (a b : α) : a ≤ b ∨ b ≤ a

  A linear order is total.

- toDecidableLE : DecidableLE α

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

- toDecidableEq : DecidableEq α

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

- toDecidableLT : DecidableLT α

  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 = compareOfLessAndEq a b

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

Instances

source
instance instIsLinearOrder_mathlib {α : Type u_1} [LinearOrder α] :
Std.IsLinearOrder α
source
theorem le_total {α : Type u_1} [LinearOrder α] (a b : α) :
a ≤ b ∨ b ≤ a
source
theorem le_of_not_ge {α : Type u_1} [LinearOrder α] {a b : α} :
¬a ≤ b → b ≤ a
source
theorem lt_of_not_ge {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b ≤ a) :
a < b
source
@[deprecated le_of_not_ge (since := "2025-05-11")]
theorem le_of_not_le {α : Type u_1} [LinearOrder α] {a b : α} :
¬a ≤ b → b ≤ a

Alias of `le_of_not_ge`.

source
theorem lt_trichotomy {α : Type u_1} [LinearOrder α] (a b : α) :
a < b ∨ a = b ∨ b < a
source
theorem le_of_not_gt {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b < a) :
a ≤ b
source
@[deprecated le_of_not_gt (since := "2025-05-11")]
theorem le_of_not_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b < a) :
a ≤ b

Alias of `le_of_not_gt`.

source
theorem lt_or_ge {α : Type u_1} [LinearOrder α] (a b : α) :
a < b ∨ b ≤ a
source
@[deprecated lt_or_ge (since := "2025-05-11")]
theorem lt_or_le {α : Type u_1} [LinearOrder α] (a b : α) :
a < b ∨ b ≤ a

Alias of `lt_or_ge`.

source
theorem le_or_gt {α : Type u_1} [LinearOrder α] (a b : α) :
a ≤ b ∨ b < a
source
@[deprecated le_or_gt (since := "2025-05-11")]
theorem le_or_lt {α : Type u_1} [LinearOrder α] (a b : α) :
a ≤ b ∨ b < a

Alias of `le_or_gt`.

source
theorem lt_or_gt_of_ne {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≠ b) :
a < b ∨ b < a
source
theorem ne_iff_lt_or_gt {α : Type u_1} [LinearOrder α] {a b : α} :
a ≠ b ↔ a < b ∨ b < a
source
theorem lt_iff_not_ge {α : Type u_1} [LinearOrder α] {a b : α} :
a < b ↔ ¬b ≤ a
source
@[simp]
theorem not_lt {α : Type u_1} [LinearOrder α] {a b : α} :
¬a < b ↔ b ≤ a
source
@[simp]
theorem not_le {α : Type u_1} [LinearOrder α] {a b : α} :
¬a ≤ b ↔ b < a
source
theorem eq_or_gt_of_not_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬a < b) :
a = b ∨ b < a
source
@[deprecated eq_or_gt_of_not_lt (since := "2025-07-27")]
theorem eq_or_lt_of_not_gt {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬a < b) :
a = b ∨ b < a

Alias of `eq_or_gt_of_not_lt`.

source
@[deprecated eq_or_gt_of_not_lt (since := "2025-05-11")]
theorem eq_or_lt_of_not_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬a < b) :
a = b ∨ b < a

Alias of `eq_or_gt_of_not_lt`.

source
theorem le_imp_le_of_lt_imp_lt {α : Type u_2} {β : Type u_3} [Preorder α] [LinearOrder β] {a b : α} {c d : β} (H : d < c → b < a) (h : a ≤ b) :
c ≤ d
source
theorem min_def {α : Type u_1} [LinearOrder α] (a b : α) :
min a b = if a ≤ b then a else b
source
theorem max_def {α : Type u_1} [LinearOrder α] (a b : α) :
max a b = if a ≤ b then b else a
source
theorem min_le_left {α : Type u_1} [LinearOrder α] (a b : α) :
min a b ≤ a
source
theorem min_le_right {α : Type u_1} [LinearOrder α] (a b : α) :
min a b ≤ b
source
theorem le_min {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c ≤ a) (h₂ : c ≤ b) :
c ≤ min a b
source
theorem le_max_left {α : Type u_1} [LinearOrder α] (a b : α) :
a ≤ max a b
source
theorem le_max_right {α : Type u_1} [LinearOrder α] (a b : α) :
b ≤ max a b
source
theorem max_le {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ c) (h₂ : b ≤ c) :
max a b ≤ c
source
theorem eq_min {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c ≤ a) (h₂ : c ≤ b) (h₃ : ∀ {d : α}, d ≤ a → d ≤ b → d ≤ c) :
c = min a b
source
theorem min_comm {α : Type u_1} [LinearOrder α] (a b : α) :
min a b = min b a
source
theorem min_assoc {α : Type u_1} [LinearOrder α] (a b c : α) :
min (min a b) c = min a (min b c)
source
theorem min_left_comm {α : Type u_1} [LinearOrder α] (a b c : α) :
min a (min b c) = min b (min a c)
source
@[simp]
theorem min_self {α : Type u_1} [LinearOrder α] (a : α) :
min a a = a
source
theorem min_eq_left {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
min a b = a
source
theorem min_eq_right {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) :
min a b = b
source
theorem eq_max {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ c) (h₂ : b ≤ c) (h₃ : ∀ {d : α}, a ≤ d → b ≤ d → c ≤ d) :
c = max a b
source
theorem max_comm {α : Type u_1} [LinearOrder α] (a b : α) :
max a b = max b a
source
theorem max_assoc {α : Type u_1} [LinearOrder α] (a b c : α) :
max (max a b) c = max a (max b c)
source
theorem max_left_comm {α : Type u_1} [LinearOrder α] (a b c : α) :
max a (max b c) = max b (max a c)
source
@[simp]
theorem max_self {α : Type u_1} [LinearOrder α] (a : α) :
max a a = a
source
theorem max_eq_left {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) :
max a b = a
source
theorem max_eq_right {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
max a b = b
source
theorem min_eq_left_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) :
min a b = a
source
theorem min_eq_right_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : b < a) :
min a b = b
source
theorem max_eq_left_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : b < a) :
max a b = a
source
theorem max_eq_right_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) :
max a b = b
source
theorem lt_min {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a < b) (h₂ : a < c) :
a < min b c
source
theorem max_lt {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a < c) (h₂ : b < c) :
max a b < c
source
theorem compare_lt_iff_lt {α : Type u_1} [LinearOrder α] {a b : α} :
compare a b = Ordering.lt ↔ a < b
source
theorem compare_gt_iff_gt {α : Type u_1} [LinearOrder α] {a b : α} :
compare a b = Ordering.gt ↔ b < a
source
theorem compare_eq_iff_eq {α : Type u_1} [LinearOrder α] {a b : α} :
compare a b = Ordering.eq ↔ a = b
source
theorem compare_le_iff_le {α : Type u_1} [LinearOrder α] {a b : α} :
compare a b ≠ Ordering.gt ↔ a ≤ b
source
theorem compare_ge_iff_ge {α : Type u_1} [LinearOrder α] {a b : α} :
compare a b ≠ Ordering.lt ↔ b ≤ a
source
theorem compare_iff {α : Type u_1} [LinearOrder α] (a b : α) {o : Ordering} :
compare a b = o ↔ o.Compares a b
source
theorem cmp_eq_compare {α : Type u_1} [LinearOrder α] (a b : α) :
cmp a b = compare a b
source
theorem cmp_eq_compareOfLessAndEq {α : Type u_1} [LinearOrder α] (a b : α) :
cmp a b = compareOfLessAndEq a b
source
instance instLawfulBCmpCompare_mathlib {α : Type u_1} [LinearOrder α] :
Std.LawfulBCmp compare