mathlib documentation

order.basic

Basic definitions about and < #

This file proves basic results about orders, provides extensive dot notation, defines useful order classes and allows to transfer order instances.

Type synonyms #

Transfering orders #

Extra classes #

Notes #

and < are highly favored over and > in mathlib. The reason is that we can formulate all lemmas using /<, and rw has trouble unifying and . Hence choosing one direction spares us useless duplication. This is enforced by a linter. See Note [nolint_ge] for more infos.

Dot notation is particularly useful on (has_le.le) and < (has_lt.lt). To that end, we provide many aliases to dot notation-less lemmas. For example, le_trans is aliased with has_le.le.trans and can be used to construct hab.trans hbc : a ≤ c when hab : a ≤ b, hbc : b ≤ c, lt_of_le_of_lt is aliased as has_le.le.trans_lt and can be used to construct hab.trans hbc : a < c when hab : a ≤ b, hbc : b < c.

TODO #

See also #

Tags #

preorder, order, partial order, poset, linear order, chain

theorem has_le.ext {α : Type u} (x y : has_le α) (h : has_le.le = has_le.le) :
x = y
theorem has_le.ext_iff {α : Type u} (x y : has_le α) :
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} [partial_order α] {a b : α} :
a bb aa = b

Alias of le_antisymm.

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

@[simp]
theorem lt_self_iff_false {α : Type u} [preorder α] (x : α) :
x < x false
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
theorem eq.not_lt {α : Type u} [partial_order α] {x y : α} (h : x = y) :
¬x < y
theorem eq.not_gt {α : Type u} [partial_order α] {x y : α} (h : x = y) :
¬y < x
@[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
@[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} [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
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
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 α] {x y : α} (h : x y) :
x < y y < x
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} [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 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} [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 α] (hca : c a) (hbd : b d) :
a bc d

monotonicity of with respect to

theorem preorder.ext {α : Type u_1} {A B : preorder α} (H : ∀ (x y : α), x y x y) :
A = B
theorem partial_order.ext {α : Type u_1} {A B : partial_order α} (H : ∀ (x y : α), x y x y) :
A = B
theorem linear_order.ext {α : Type u_1} {A B : linear_order α} (H : ∀ (x y : α), x y x y) :
A = B
@[simp]
def order.preimage {α : Sort u_1} {β : Sort u_2} (f : α → β) (s : β → β → Prop) (x y : α) :
Prop

Given a relation R on β and a function f : α → β, the preimage relation on α is defined by x ≤ y ↔ f x ≤ f y. It is the unique relation on α making f a rel_embedding (assuming f is injective).

Equations
@[instance]
def order.preimage.decidable {α : Sort u_1} {β : Sort u_2} (f : α → β) (s : β → β → Prop) [H : decidable_rel s] :

The preimage of a decidable order is decidable.

Equations

Order dual #

def order_dual (α : Type u_1) :
Type u_1

Type synonym to equip a type with the dual order: means and < means >.

Equations
@[instance]
def order_dual.nonempty (α : Type u_1) [h : nonempty α] :
@[instance]
def order_dual.subsingleton (α : Type u_1) [h : subsingleton α] :
@[instance]
def order_dual.has_le (α : Type u_1) [has_le α] :
Equations
@[instance]
def order_dual.has_lt (α : Type u_1) [has_lt α] :
Equations
@[instance]
def order_dual.has_zero (α : Type u_1) [has_zero α] :
Equations
theorem order_dual.dual_le {α : Type u} [has_le α] {a b : α} :
a b b a
theorem order_dual.dual_lt {α : Type u} [has_lt α] {a b : α} :
a < b b < a
@[instance]
def order_dual.preorder (α : Type u_1) [preorder α] :
Equations
@[instance]
def order_dual.inhabited {α : Type u} [inhabited α] :
Equations
theorem order_dual.preorder.dual_dual (α : Type u_1) [H : preorder α] :

Order instances on the function space #

@[instance]
def pi.preorder {ι : Type u} {α : ι → Type v} [Π (i : ι), preorder (α i)] :
preorder (Π (i : ι), α i)
Equations
theorem pi.le_def {ι : Type u} {α : ι → Type v} [Π (i : ι), preorder (α i)] {x y : Π (i : ι), α i} :
x y ∀ (i : ι), x i y i
theorem pi.lt_def {ι : Type u} {α : ι → Type v} [Π (i : ι), preorder (α i)] {x y : Π (i : ι), α i} :
x < y x y ∃ (i : ι), x i < y i
theorem le_update_iff {ι : Type u} {α : ι → Type v} [Π (i : ι), preorder (α i)] [decidable_eq ι] {x y : Π (i : ι), α i} {i : ι} {a : α i} :
x function.update y i a x i a ∀ (j : ι), j ix j y j
theorem update_le_iff {ι : Type u} {α : ι → Type v} [Π (i : ι), preorder (α i)] [decidable_eq ι] {x y : Π (i : ι), α i} {i : ι} {a : α i} :
function.update x i a y a y i ∀ (j : ι), j ix j y j
theorem update_le_update_iff {ι : Type u} {α : ι → Type v} [Π (i : ι), preorder (α i)] [decidable_eq ι] {x y : Π (i : ι), α i} {i : ι} {a b : α i} :
function.update x i a function.update y i b a b ∀ (j : ι), j ix j y j
@[instance]
def pi.partial_order {ι : Type u} {α : ι → Type v} [Π (i : ι), partial_order (α i)] :
partial_order (Π (i : ι), α i)
Equations

Lifts of order instances #

def preorder.lift {α : Type u_1} {β : Type u_2} [preorder β] (f : α → β) :

Transfer a preorder on β to a preorder on α using a function f : α → β. See note [reducible non-instances].

Equations
def partial_order.lift {α : Type u_1} {β : Type u_2} [partial_order β] (f : α → β) (inj : function.injective f) :

Transfer a partial_order on β to a partial_order on α using an injective function f : α → β. See note [reducible non-instances].

Equations
def linear_order.lift {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (inj : function.injective f) :

Transfer a linear_order on β to a linear_order on α using an injective function f : α → β. See note [reducible non-instances].

Equations
@[instance]
def subtype.preorder {α : Type u_1} [preorder α] (p : α → Prop) :
Equations
@[simp]
theorem subtype.mk_le_mk {α : Type u_1} [preorder α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y} :
x, hx⟩ y, hy⟩ x y
@[simp]
theorem subtype.mk_lt_mk {α : Type u_1} [preorder α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y} :
x, hx⟩ < y, hy⟩ x < y
@[simp]
theorem subtype.coe_le_coe {α : Type u_1} [preorder α] {p : α → Prop} {x y : subtype p} :
x y x y
@[simp]
theorem subtype.coe_lt_coe {α : Type u_1} [preorder α] {p : α → Prop} {x y : subtype p} :
x < y x < y
@[instance]
def subtype.linear_order {α : Type u_1} [linear_order α] (p : α → Prop) :
Equations
@[instance]
def prod.has_le (α : Type u) (β : Type v) [has_le α] [has_le β] :
has_le × β)
Equations
theorem prod.le_def {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {x y : α × β} :
x y x.fst y.fst x.snd y.snd
@[simp]
theorem prod.mk_le_mk {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {x₁ x₂ : α} {y₁ y₂ : β} :
(x₁, y₁) (x₂, y₂) x₁ x₂ y₁ y₂
@[instance]
def prod.preorder (α : Type u) (β : Type v) [preorder α] [preorder β] :
preorder × β)
Equations
@[instance]
def prod.partial_order (α : Type u) (β : Type v) [partial_order α] [partial_order β] :

The pointwise partial order on a product. (The lexicographic ordering is defined in order/lexicographic.lean, and the instances are available via the type synonym lex α β = α × β.)

Equations

Additional order classes #

@[class]
structure no_top_order (α : Type u) [preorder α] :
Prop
  • no_top : ∀ (a : α), ∃ (a' : α), a < a'

Order without a maximal element. Sometimes called cofinal.

Instances
theorem no_top {α : Type u} [preorder α] [no_top_order α] (a : α) :
∃ (a' : α), a < a'
@[instance]
def nonempty_gt {α : Type u} [preorder α] [no_top_order α] (a : α) :
nonempty {x // a < x}
def is_top {α : Type u} [has_le α] (a : α) :
Prop

a : α is a top element of α if it is greater than or equal to any other element of α. This predicate is useful, e.g., to make some statements and proofs work in both cases [order_top α] and [no_top_order α].

Equations
@[simp]
theorem not_is_top {α : Type u} [preorder α] [no_top_order α] (a : α) :
theorem is_top.unique {α : Type u} [partial_order α] {a b : α} (ha : is_top a) (hb : a b) :
a = b
@[class]
structure no_bot_order (α : Type u) [preorder α] :
Prop
  • no_bot : ∀ (a : α), ∃ (a' : α), a' < a

Order without a minimal element. Sometimes called coinitial or dense.

Instances
theorem no_bot {α : Type u} [preorder α] [no_bot_order α] (a : α) :
∃ (a' : α), a' < a
def is_bot {α : Type u} [has_le α] (a : α) :
Prop

a : α is a bottom element of α if it is less than or equal to any other element of α. This predicate is useful, e.g., to make some statements and proofs work in both cases [order_bot α] and [no_bot_order α].

Equations
@[simp]
theorem not_is_bot {α : Type u} [preorder α] [no_bot_order α] (a : α) :
theorem is_bot.unique {α : Type u} [partial_order α] {a b : α} (ha : is_bot a) (hb : b a) :
a = b
@[instance]
@[instance]
@[instance]
def nonempty_lt {α : Type u} [preorder α] [no_bot_order α] (a : α) :
nonempty {x // x < a}
@[class]
structure densely_ordered (α : Type u) [preorder α] :
Prop
  • dense : ∀ (a₁ a₂ : α), a₁ < a₂(∃ (a : α), a₁ < a a < a₂)

An order is dense if there is an element between any pair of distinct elements.

Instances
theorem exists_between {α : Type u} [preorder α] [densely_ordered α] {a₁ a₂ : α} :
a₁ < a₂(∃ (a : α), a₁ < a a < a₂)
@[instance]
theorem le_of_forall_le_of_dense {α : Type u} [linear_order α] [densely_ordered α] {a₁ a₂ : α} (h : ∀ (a : α), a₂ < aa₁ a) :
a₁ a₂
theorem eq_of_le_of_forall_le_of_dense {α : Type u} [linear_order α] [densely_ordered α] {a₁ a₂ : α} (h₁ : a₂ a₁) (h₂ : ∀ (a : α), a₂ < aa₁ a) :
a₁ = a₂
theorem le_of_forall_ge_of_dense {α : Type u} [linear_order α] [densely_ordered α] {a₁ a₂ : α} (h : ∀ (a₃ : α), a₃ < a₁a₃ a₂) :
a₁ a₂
theorem eq_of_le_of_forall_ge_of_dense {α : Type u} [linear_order α] [densely_ordered α] {a₁ a₂ : α} (h₁ : a₂ a₁) (h₂ : ∀ (a₃ : α), a₃ < a₁a₃ a₂) :
a₁ = a₂
theorem dense_or_discrete {α : Type u} [linear_order α] (a₁ a₂ : α) :
(∃ (a : α), a₁ < a a < a₂) (∀ (a : α), a₁ < aa₂ a) ∀ (a : α), a < a₂a a₁

Linear order from a total partial order #

def as_linear_order (α : Type u) :
Type u

Type synonym to create an instance of linear_order from a partial_order and is_total α (≤)

Equations
@[instance]
Equations