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.

source

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

x ≤ x

A version of le_refl where the argument is implicit

source

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.

source

theorem eq.trans_le {α : Type u} [preorder α] {x y z : α} (h1 : x = y) (h2 : y ≤ z) :

x ≤ z

source

@[nolint]

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

y ≥ x

source

theorem has_le.le.trans_eq {α : Type u} [preorder α] {x y z : α} (h1 : x ≤ y) (h2 : y = z) :

x ≤ z

source

@[nolint]

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

y > x

source

theorem has_lt.lt.false {α : Type u} [preorder α] {x : α} (a : x < x) :

false

source

@[nolint]

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

y ≤ x

source

@[nolint]

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

y < x

source

@[nolint]

theorem ge_of_eq {α : Type u} [preorder α] {a b : α} (h : a = b) :

a ≥ b

source

@[simp, nolint]

theorem ge_iff_le {α : Type u} [preorder α] {a b : α} :

a ≥ b ↔ b ≤ a

source

@[simp, nolint]

theorem gt_iff_lt {α : Type u} [preorder α] {a b : α} :

a > b ↔ b < a

source

theorem not_le_of_lt {α : Type u} [preorder α] {a b : α} (h : a < b) :

¬b ≤ a

source

theorem not_lt_of_le {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :

¬b < a

source

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

a ≤ b ↔ a = b ∨ a < b

source

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

a < b ↔ a ≤ b ∧ a ≠ b

source

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

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

source

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

a = b ∨ a < b

source

theorem lt_of_not_ge' {α : Type u} [linear_order α] {a b : α} (h : ¬b ≤ a) :

a < b

source

theorem lt_iff_not_ge' {α : Type u} [linear_order α] {x y : α} :

x < y ↔ ¬y ≤ x

source

theorem le_of_not_lt {α : Type u} [linear_order α] {a b : α} (a_1 : ¬a < b) :

b ≤ a

source

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

a < b ∨ b ≤ a

source

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

a ≤ b ∨ b < a

source

theorem has_le.le.lt_or_le {α : Type u} [linear_order α] {a b : α} (h : a ≤ b) (c : α) :

a < c ∨ c ≤ b

source

theorem has_le.le.le_or_lt {α : Type u} [linear_order α] {a b : α} (h : a ≤ b) (c : α) :

a ≤ c ∨ c < b

source

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

¬a < b ↔ a = b ∨ b < a

source

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

∃ (c : α), a ≤ c ∧ b ≤ c

source

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

source

theorem le_imp_le_of_lt_imp_lt {α : Type u} {β : Type u_1} [preorder α] [linear_order β] {a b : α} {c d : β} (H : d < c → b < a) (h : a ≤ b) :

c ≤ d

source

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

source

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

source

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

source

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)

source

theorem eq_of_forall_le_iff {α : Type u} [partial_order α] {a b : α} (H : ∀ (c : α), c ≤ a ↔ c ≤ b) :

a = b

source

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

a ≤ b

source

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

b ≤ a

source

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

a ≤ b

source

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

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

source

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

b ≤ a

source

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

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

source

theorem eq_of_forall_ge_iff {α : Type u} [partial_order α] {a b : α} (H : ∀ (c : α), a ≤ c ↔ b ≤ c) :

a = b

source

theorem le_implies_le_of_le_of_le {α : Type u} {a b c d : α} [preorder α] (h₀ : c ≤ a) (h₁ : b ≤ d) (a_1 : a ≤ b) :

c ≤ d

monotonicity of ≤ with respect to →

source

theorem decidable.le_imp_le_iff_lt_imp_lt {α : Type u} {β : Type u_1} [linear_order α] [decidable_linear_order β] {a b : α} {c d : β} :

a ≤ b → c ≤ d ↔ d < c → b < a

source

theorem decidable.le_iff_le_iff_lt_iff_lt {α : Type u} {β : Type u_1} [decidable_linear_order α] [decidable_linear_order β] {a b : α} {c d : β} :

a ≤ b ↔ c ≤ d ↔ (b < a ↔ d < c)

source

@[simp]

def ordering.compares {α : Type u} [has_lt α] (a : ordering) (a_1 a_2 : α) :

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)

source

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

o = ordering.lt ↔ a < b

source

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

o = ordering.eq ↔ a = b

source

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

o = ordering.gt ↔ b < a

source

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

o₁ = o₂

source

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'

source

theorem ordering.swap_or_else (o₁ o₂ : ordering) :

(o₁.or_else o₂).swap = o₁.swap.or_else o₂.swap

source

theorem ordering.or_else_eq_lt (o₁ o₂ : ordering) :

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

source

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

(cmp a b).compares a b

source

theorem cmp_swap {α : Type u} [preorder α] [decidable_rel has_lt.lt] (a b : α) :

(cmp a b).swap = cmp b a