mathlib documentation

algebra.order

Lemmas about inequalities #

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 ≤ b → b ≤ c → a ≤ c

Alias of le_trans.

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

a ≤ b → b < c → a < c

Alias of lt_of_le_of_lt.

theorem has_le.le.antisymm {α : Type u} [partial_order α] {a b : α} :

a ≤ b → b ≤ a → a = b

Alias of le_antisymm.

theorem has_le.le.lt_of_ne {α : Type u} [partial_order α] {a b : α} :

a ≤ b → a ≠ b → a < b

Alias of lt_of_le_of_ne.

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

a ≤ b → ¬b ≤ a → a < b

Alias of lt_of_le_not_le.

theorem has_le.le.lt_or_eq {α : Type u} [partial_order α] {a b : α} :

a ≤ b → a < b ∨ a = b

Alias of lt_or_eq_of_le.

@[nolint]

theorem has_le.le.lt_or_eq_dec {α : Type u} [partial_order α] [decidable_rel has_le.le] {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 < b → a ≤ b

Alias of le_of_lt.

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

a < b → b < c → a < c

Alias of lt_trans.

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

a < b → b ≤ c → a < 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 = b → a ≤ 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

@[protected]

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

@[protected, 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} [partial_order α] {x y : α} (h : x ≤ y) :

x < y ↔ x ≠ y

theorem has_le.le.le_iff_eq {α : Type u} [partial_order α] {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

@[protected, nolint]

theorem has_lt.lt.gt {α : Type u} [has_lt α] {x y : α} (h : x < y) :

y > x

@[protected]

theorem has_lt.lt.false {α : Type u} [preorder α] {x : α} :

x < x → false

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

@[protected, nolint]

theorem ge.le {α : Type u} [has_le α] {x y : α} (h : x ≥ y) :

y ≤ x

@[protected, 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) :

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

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.

@[protected]

theorem decidable.le_iff_eq_or_lt {α : Type u} [partial_order α] [decidable_rel has_le.le] {a b : α} :

a ≤ b ↔ a = b ∨ a < b

theorem le_iff_eq_or_lt {α : Type u} [partial_order α] {a b : α} :

a ≤ b ↔ a = b ∨ a < b

theorem lt_iff_le_and_ne {α : Type u} [partial_order α] {a b : α} :

a < b ↔ a ≤ b ∧ a ≠ b

@[protected]

theorem decidable.eq_iff_le_not_lt {α : Type u} [partial_order α] [decidable_rel has_le.le] {a b : α} :

a = b ↔ a ≤ b ∧ ¬a < b

theorem eq_iff_le_not_lt {α : Type u} [partial_order α] {a b : α} :

a = b ↔ a ≤ b ∧ ¬a < b

theorem eq_or_lt_of_le {α : Type u} [partial_order α] {a b : α} (h : a ≤ b) :

a = b ∨ a < b

@[nolint]

theorem has_le.le.eq_or_lt_dec {α : Type u} [partial_order α] [decidable_rel has_le.le] {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} [partial_order α] {a b : α} (h : a ≤ b) :

a = b ∨ a < b

Alias of eq_or_lt_of_le.

theorem ne.le_iff_lt {α : Type u} [partial_order α] {a b : α} (h : a ≠ b) :

a ≤ b ↔ a < b

@[protected]

theorem decidable.ne_iff_lt_iff_le {α : Type u} [partial_order α] [decidable_rel has_le.le] {a b : α} :

a ≠ b ↔ a < b ↔ a ≤ b

@[simp]

theorem ne_iff_lt_iff_le {α : Type u} [partial_order α] {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 ≤ b → c ≤ 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 ≤ b → c ≤ d ↔ d < c → b < 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} [partial_order α] {a b : α} (H : ∀ (c : α), c ≤ a ↔ c ≤ b) :

a = b

theorem le_of_forall_le {α : Type u} [preorder α] {a b : α} (H : ∀ (c : α), c ≤ a → c ≤ b) :

a ≤ b

theorem le_of_forall_le' {α : Type u} [preorder α] {a b : α} (H : ∀ (c : α), a ≤ c → b ≤ c) :

b ≤ a

theorem le_of_forall_lt {α : Type u} [linear_order α] {a b : α} (H : ∀ (c : α), c < a → c < b) :

a ≤ b

theorem forall_lt_iff_le {α : Type u} [linear_order α] {a b : α} :

(∀ ⦃c : α⦄, c < a → c < b) ↔ a ≤ b

theorem le_of_forall_lt' {α : Type u} [linear_order α] {a b : α} (H : ∀ (c : α), a < c → b < c) :

b ≤ a

theorem forall_lt_iff_le' {α : Type u} [linear_order α] {a b : α} :

(∀ ⦃c : α⦄, a < c → b < c) ↔ b ≤ a

theorem eq_of_forall_ge_iff {α : Type u} [partial_order α] {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 ≤ b → c ≤ d

monotonicity of ≤ with respect to →

def cmp_le {α : Type u_1} [has_le α] [decidable_rel has_le.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

cmp_le x y = ite (x ≤ y) (ite (y ≤ x) ordering.eq ordering.lt) ordering.gt

theorem cmp_le_swap {α : Type u_1} [has_le α] [is_total α has_le.le] [decidable_rel has_le.le] (x y : α) :

(cmp_le x y).swap = cmp_le y x

theorem cmp_le_eq_cmp {α : Type u_1} [preorder α] [is_total α has_le.le] [decidable_rel has_le.le] [decidable_rel has_lt.lt] (x y : α) :

cmp_le x 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

ordering.gt.compares a b = (a > b)
ordering.eq.compares a b = (a = b)
ordering.lt.compares a b = (a < b)

theorem ordering.compares_swap {α : Type u} [has_lt α] {a b : α} {o : ordering} :

o.swap.compares a b ↔ o.compares b a

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

o.swap.compares a b → o.compares b a

Alias of compares_swap.

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

o.compares b a → o.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 → (o = ordering.lt ↔ a < b)

theorem ordering.compares.ne_lt {α : Type u} [preorder α] {o : ordering} {a b : α} :

o.compares a b → (o ≠ ordering.lt ↔ b ≤ a)

theorem ordering.compares.eq_eq {α : Type u} [preorder α] {o : ordering} {a b : α} :

o.compares a b → (o = ordering.eq ↔ a = b)

theorem ordering.compares.eq_gt {α : Type u} [preorder α] {o : ordering} {a b : α} (h : o.compares a b) :

o = ordering.gt ↔ b < a

theorem ordering.compares.ne_gt {α : Type u} [preorder α] {o : ordering} {a b : α} (h : o.compares a b) :

o ≠ ordering.gt ↔ a ≤ b

theorem ordering.compares.le_total {α : Type u} [preorder α] {a b : α} {o : ordering} :

o.compares a b → a ≤ b ∨ b ≤ a

theorem ordering.compares.le_antisymm {α : Type u} [preorder α] {a b : α} {o : ordering} :

o.compares a b → a ≤ b → b ≤ a → a = b

theorem ordering.compares.inj {α : Type u} [preorder α] {o₁ o₂ : ordering} {a b : α} :

o₁.compares a b → o₂.compares a b → o₁ = 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 b → o.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) :

o₁.or_else o₂ = ordering.lt ↔ o₁ = ordering.lt ∨ o₁ = ordering.eq ∧ o₂ = ordering.lt

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

(cmp a b).compares a b

theorem cmp_swap {α : Type u} [preorder α] [decidable_rel has_lt.lt] (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) :

linear_order α

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

Equations

linear_order_of_compares cmp h = {le := preorder.le _inst_1, lt := preorder.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (a b : α), decidable_of_iff (cmp a b ≠ ordering.gt) _, decidable_eq := λ (a b : α), decidable_of_iff (cmp a b = ordering.eq) _, decidable_lt := λ (a b : α), decidable_of_iff (cmp a b = ordering.lt) _}

@[simp]

theorem cmp_eq_lt_iff {α : Type u} [linear_order α] (x y : α) :

cmp x y = ordering.lt ↔ x < y

@[simp]

theorem cmp_eq_eq_iff {α : Type u} [linear_order α] (x y : α) :

cmp x y = ordering.eq ↔ x = y

@[simp]

theorem cmp_eq_gt_iff {α : Type u} [linear_order α] (x y : α) :

cmp x y = ordering.gt ↔ y < x

@[simp]

theorem cmp_self_eq_eq {α : Type u} [linear_order α] (x : α) :

cmp x x = ordering.eq

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'