# mathlibdocumentation

algebra.order

This file contains some lemmas about ≤/≥/</>, and cmp.

• We simplify a ≥ b and a > b to b ≤ a and b < a, respectively. This way we can formulate all lemmas using ≤/< avoiding duplication.

• In some cases we introduce dot syntax aliases so that, e.g., from (hab : a ≤ b) (hbc : b ≤ c) (hbc' : b < c) one can prove hab.trans hbc : a ≤ c and hab.trans_lt hbc' : a < c.

theorem has_le.le.trans {α : Type u} [preorder α] {a b c : α} :
a bb ca c

Alias of le_trans.

theorem has_le.le.trans_lt {α : Type u} [preorder α] {a b c : α} :
a bb < ca < c

Alias of lt_of_le_of_lt.

theorem has_le.le.antisymm {α : Type u} {a b : α} :
a bb aa = b

Alias of le_antisymm.

theorem has_le.le.lt_of_ne {α : Type u} {a b : α} :
a ba ba < b

Alias of lt_of_le_of_ne.

theorem has_le.le.lt_of_not_le {α : Type u} [preorder α] {a b : α} :
a b¬b aa < b

Alias of lt_of_le_not_le.

theorem has_le.le.lt_or_eq {α : Type u} {a b : α} :
a ba < b a = b

Alias of lt_or_eq_of_le.

@[nolint]
theorem has_le.le.lt_or_eq_dec {α : Type u} {a b : α} (hab : a b) :
a < b a = b

Alias of decidable.lt_or_eq_of_le.

theorem has_lt.lt.le {α : Type u} [preorder α] {a b : α} :
a < ba b

Alias of le_of_lt.

theorem has_lt.lt.trans {α : Type u} [preorder α] {a b c : α} :
a < bb < ca < c

Alias of lt_trans.

theorem has_lt.lt.trans_le {α : Type u} [preorder α] {a b c : α} :
a < bb ca < c

Alias of lt_of_lt_of_le.

theorem has_lt.lt.ne {α : Type u} [preorder α] {a b : α} (h : a < b) :
a b

Alias of ne_of_lt.

theorem has_lt.lt.asymm {α : Type u} [preorder α] {a b : α} (h : a < b) :
¬b < a

Alias of lt_asymm.

theorem has_lt.lt.not_lt {α : Type u} [preorder α] {a b : α} (h : a < b) :
¬b < a

Alias of lt_asymm.

theorem eq.le {α : Type u} [preorder α] {a b : α} :
a = ba b

Alias of le_of_eq.

theorem le_rfl {α : Type u} [preorder α] {x : α} :
x x

A version of le_refl where the argument is implicit

theorem eq.ge {α : Type u} [preorder α] {x y : α} (h : x = y) :
y x

If x = y then y ≤ x. Note: this lemma uses y ≤ x instead of x ≥ y, because le is used almost exclusively in mathlib.

theorem eq.trans_le {α : Type u} [preorder α] {x y z : α} (h1 : x = y) (h2 : y z) :
x z
@[nolint]
theorem has_le.le.ge {α : Type u} [has_le α] {x y : α} (h : x y) :
y x
theorem has_le.le.trans_eq {α : Type u} [preorder α] {x y z : α} (h1 : x y) (h2 : y = z) :
x z
theorem has_le.le.lt_iff_ne {α : Type u} {x y : α} (h : x y) :
x < y x y
theorem has_le.le.le_iff_eq {α : Type u} {x y : α} (h : x y) :
y x y = x
theorem has_le.le.lt_or_le {α : Type u} [linear_order α] {a b : α} (h : a b) (c : α) :
a < c c b
theorem has_le.le.le_or_lt {α : Type u} [linear_order α] {a b : α} (h : a b) (c : α) :
a c c < b
theorem has_le.le.le_or_le {α : Type u} [linear_order α] {a b : α} (h : a b) (c : α) :
a c c b
@[nolint]
theorem has_lt.lt.gt {α : Type u} [has_lt α] {x y : α} (h : x < y) :
y > x
theorem has_lt.lt.false {α : Type u} [preorder α] {x : α} :
x < xfalse
theorem has_lt.lt.ne' {α : Type u} [preorder α] {x y : α} (h : x < y) :
y x
theorem has_lt.lt.lt_or_lt {α : Type u} [linear_order α] {x y : α} (h : x < y) (z : α) :
x < z z < y
@[nolint]
theorem ge.le {α : Type u} [has_le α] {x y : α} (h : x y) :
y x
@[nolint]
theorem gt.lt {α : Type u} [has_lt α] {x y : α} (h : x > y) :
y < x
@[nolint]
theorem ge_of_eq {α : Type u} [preorder α] {a b : α} (h : a = b) :
a b
@[simp, nolint]
theorem ge_iff_le {α : Type u} [preorder α] {a b : α} :
a b b a
@[simp, nolint]
theorem gt_iff_lt {α : Type u} [preorder α] {a b : α} :
a > b b < a
theorem not_le_of_lt {α : Type u} [preorder α] {a b : α} (h : a < b) :
¬b a
theorem has_lt.lt.not_le {α : Type u} [preorder α] {a b : α} (h : a < b) :
¬b a

Alias of not_le_of_lt.

theorem not_lt_of_le {α : Type u} [preorder α] {a b : α} (h : a b) :
¬b < a
theorem has_le.le.not_lt {α : Type u} [preorder α] {a b : α} (h : a b) :
¬b < a

Alias of not_lt_of_le.

theorem decidable.le_iff_eq_or_lt {α : Type u} {a b : α} :
a b a = b a < b
theorem le_iff_eq_or_lt {α : Type u} {a b : α} :
a b a = b a < b
theorem lt_iff_le_and_ne {α : Type u} {a b : α} :
a < b a b a b
theorem decidable.eq_iff_le_not_lt {α : Type u} {a b : α} :
a = b a b ¬a < b
theorem eq_iff_le_not_lt {α : Type u} {a b : α} :
a = b a b ¬a < b
theorem eq_or_lt_of_le {α : Type u} {a b : α} (h : a b) :
a = b a < b
@[nolint]
theorem has_le.le.eq_or_lt_dec {α : Type u} {a b : α} (hab : a b) :
a = b a < b

Alias of decidable.eq_or_lt_of_le.

theorem has_le.le.eq_or_lt {α : Type u} {a b : α} (h : a b) :
a = b a < b

Alias of eq_or_lt_of_le.

theorem ne.le_iff_lt {α : Type u} {a b : α} (h : a b) :
a b a < b
theorem decidable.ne_iff_lt_iff_le {α : Type u} {a b : α} :
a b a < b a b
@[simp]
theorem ne_iff_lt_iff_le {α : Type u} {a b : α} :
a b a < b a b
theorem lt_of_not_ge' {α : Type u} [linear_order α] {a b : α} (h : ¬b a) :
a < b
theorem lt_iff_not_ge' {α : Type u} [linear_order α] {x y : α} :
x < y ¬y x
theorem ne.lt_or_lt {α : Type u} [linear_order α] {a b : α} (h : a b) :
a < b b < a
theorem not_lt_iff_eq_or_lt {α : Type u} [linear_order α] {a b : α} :
¬a < b a = b b < a
theorem exists_ge_of_linear {α : Type u} [linear_order α] (a b : α) :
∃ (c : α), a c b c
theorem lt_imp_lt_of_le_imp_le {α : Type u} {β : Type u_1} [linear_order α] [preorder β] {a b : α} {c d : β} (H : a bc d) (h : d < c) :
b < a
theorem le_imp_le_iff_lt_imp_lt {α : Type u} {β : Type u_1} [linear_order α] [linear_order β] {a b : α} {c d : β} :
a bc d d < cb < a
theorem lt_iff_lt_of_le_iff_le' {α : Type u} {β : Type u_1} [preorder α] [preorder β] {a b : α} {c d : β} (H : a b c d) (H' : b a d c) :
b < a d < c
theorem lt_iff_lt_of_le_iff_le {α : Type u} {β : Type u_1} [linear_order α] [linear_order β] {a b : α} {c d : β} (H : a b c d) :
b < a d < c
theorem le_iff_le_iff_lt_iff_lt {α : Type u} {β : Type u_1} [linear_order α] [linear_order β] {a b : α} {c d : β} :
a b c d (b < a d < c)
theorem eq_of_forall_le_iff {α : Type u} {a b : α} (H : ∀ (c : α), c a c b) :
a = b
theorem le_of_forall_le {α : Type u} [preorder α] {a b : α} (H : ∀ (c : α), c ac b) :
a b
theorem le_of_forall_le' {α : Type u} [preorder α] {a b : α} (H : ∀ (c : α), a cb c) :
b a
theorem le_of_forall_lt {α : Type u} [linear_order α] {a b : α} (H : ∀ (c : α), c < ac < b) :
a b
theorem forall_lt_iff_le {α : Type u} [linear_order α] {a b : α} :
(∀ ⦃c : α⦄, c < ac < b) a b
theorem le_of_forall_lt' {α : Type u} [linear_order α] {a b : α} (H : ∀ (c : α), a < cb < c) :
b a
theorem forall_lt_iff_le' {α : Type u} [linear_order α] {a b : α} :
(∀ ⦃c : α⦄, a < cb < c) b a
theorem eq_of_forall_ge_iff {α : Type u} {a b : α} (H : ∀ (c : α), a c b c) :
a = b
theorem le_implies_le_of_le_of_le {α : Type u} {a b c d : α} [preorder α] (h₀ : c a) (h₁ : b d) :
a bc d

monotonicity of ≤ with respect to →

def cmp_le {α : Type u_1} [has_le α] (x y : α) :

Like cmp, but uses a ≤ on the type instead of <. Given two elements x and y, returns a three-way comparison result ordering.

Equations
theorem cmp_le_swap {α : Type u_1} [has_le α] (x y : α) :
(cmp_le x y).swap = x
theorem cmp_le_eq_cmp {α : Type u_1} [preorder α] (x y : α) :
y = cmp x y
@[simp]
def ordering.compares {α : Type u} [has_lt α] :
orderingα → α → Prop

compares o a b means that a and b have the ordering relation o between them, assuming that the relation a < b is defined

Equations
• = (a > b)
• = (a = b)
• = (a < b)
theorem ordering.compares_swap {α : Type u} [has_lt α] {a b : α} {o : ordering} :
theorem ordering.compares.of_swap {α : Type u} [has_lt α] {a b : α} {o : ordering} :
o.swap.compares a bo.compares b a

Alias of compares_swap.

theorem ordering.compares.swap {α : Type u} [has_lt α] {a b : α} {o : ordering} :
o.compares b ao.swap.compares a b

Alias of compares_swap.

theorem ordering.swap_eq_iff_eq_swap {o o' : ordering} :
o.swap = o' o = o'.swap
theorem ordering.compares.eq_lt {α : Type u} [preorder α] {o : ordering} {a b : α} :
o.compares a b a < b)
theorem ordering.compares.ne_lt {α : Type u} [preorder α] {o : ordering} {a b : α} :
o.compares a b b a)
theorem ordering.compares.eq_eq {α : Type u} [preorder α] {o : ordering} {a b : α} :
o.compares a b a = b)
theorem ordering.compares.eq_gt {α : Type u} [preorder α] {o : ordering} {a b : α} (h : o.compares a b) :
b < a
theorem ordering.compares.ne_gt {α : Type u} [preorder α] {o : ordering} {a b : α} (h : o.compares a b) :
a b
theorem ordering.compares.le_total {α : Type u} [preorder α] {a b : α} {o : ordering} :
o.compares a ba b b a
theorem ordering.compares.le_antisymm {α : Type u} [preorder α] {a b : α} {o : ordering} :
o.compares a ba bb aa = b
theorem ordering.compares.inj {α : Type u} [preorder α] {o₁ o₂ : ordering} {a b : α} :
o₁.compares a bo₂.compares a bo₁ = o₂
theorem ordering.compares_iff_of_compares_impl {α : Type u} {β : Type u_1} [linear_order α] [preorder β] {a b : α} {a' b' : β} (h : ∀ {o : ordering}, o.compares a bo.compares a' b') (o : ordering) :
o.compares a b o.compares a' b'
theorem ordering.swap_or_else (o₁ o₂ : ordering) :
(o₁.or_else o₂).swap = o₁.swap.or_else o₂.swap
theorem ordering.or_else_eq_lt (o₁ o₂ : ordering) :
theorem cmp_compares {α : Type u} [linear_order α] (a b : α) :
(cmp a b).compares a b
theorem cmp_swap {α : Type u} [preorder α] (a b : α) :
(cmp a b).swap = cmp b a
def linear_order_of_compares {α : Type u} [preorder α] (cmp : α → α → ordering) (h : ∀ (a b : α), (cmp a b).compares a b) :

Generate a linear order structure from a preorder and cmp function.

Equations
@[simp]
theorem cmp_eq_lt_iff {α : Type u} [linear_order α] (x y : α) :
@[simp]
theorem cmp_eq_eq_iff {α : Type u} [linear_order α] (x y : α) :
@[simp]
theorem cmp_eq_gt_iff {α : Type u} [linear_order α] (x y : α) :
@[simp]
theorem cmp_self_eq_eq {α : Type u} [linear_order α] (x : α) :
theorem cmp_eq_cmp_symm {α : Type u} [linear_order α] {x y : α} {β : Type u_1} [linear_order β] {x' y' : β} :
cmp x y = cmp x' y' cmp y x = cmp y' x'
theorem lt_iff_lt_of_cmp_eq_cmp {α : Type u} [linear_order α] {x y : α} {β : Type u_1} [linear_order β] {x' y' : β} (h : cmp x y = cmp x' y') :
x < y x' < y'
theorem le_iff_le_of_cmp_eq_cmp {α : Type u} [linear_order α] {x y : α} {β : Type u_1} [linear_order β] {x' y' : β} (h : cmp x y = cmp x' y') :
x y x' y'