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 #

Tags #

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

theorem ge_antisymm {α : Type u} [partial_order α] {a b : α} (hab : a b) (hba : b a) :
b = a
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.antisymm' {α : Type u} [partial_order α] {a b : α} (hab : a b) (hba : b a) :
b = a

Alias of ge_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
@[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
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
@[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 < 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
@[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) :
¬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 ne_of_not_le {α : Type u} [preorder α] {a b : α} (h : ¬a b) :
a b
@[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 eq_of_le_of_not_lt {α : Type u} [partial_order α] {a b : α} (hab : a b) (hba : ¬a < b) :
a = b
theorem eq_of_ge_of_not_gt {α : Type u} [partial_order α] {a b : α} (hab : a b) (hba : ¬a < b) :
b = a
theorem has_le.le.eq_of_not_lt {α : Type u} [partial_order α] {a b : α} (hab : a b) (hba : ¬a < b) :
a = b

Alias of eq_of_le_of_not_lt.

theorem has_le.le.eq_of_not_gt {α : Type u} [partial_order α] {a b : α} (hab : a b) (hba : ¬a < b) :
b = a

Alias of eq_of_ge_of_not_gt.

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 α] {x y : α} (h : x y) :
x < y y < x
@[simp]
theorem lt_or_lt_iff_ne {α : Type u} [linear_order α] {x y : α} :
x < y y < x x y

A version of ne_iff_lt_or_gt with LHS and RHS reversed.

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
@[protected, 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
@[protected, instance]
def order_dual.nonempty (α : Type u_1) [h : nonempty α] :
@[protected, instance]
def order_dual.subsingleton (α : Type u_1) [h : subsingleton α] :
@[protected, instance]
def order_dual.has_le (α : Type u_1) [has_le α] :
Equations
@[protected, instance]
def order_dual.has_lt (α : Type u_1) [has_lt α] :
Equations
@[protected, 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
@[protected, instance]
def order_dual.preorder (α : Type u_1) [preorder α] :
Equations
@[protected, 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 #

@[protected, instance]
def pi.has_le {ι : Type u} {α : ι → Type v} [Π (i : ι), has_le (α i)] :
has_le (Π (i : ι), α i)
Equations
theorem pi.le_def {ι : Type u} {α : ι → Type v} [Π (i : ι), has_le (α i)] {x y : Π (i : ι), α i} :
x y ∀ (i : ι), x i y i
@[protected, instance]
def pi.preorder {ι : Type u} {α : ι → Type v} [Π (i : ι), preorder (α i)] :
preorder (Π (i : ι), α i)
Equations
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
@[protected, 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
@[protected, 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, norm_cast]
theorem subtype.coe_le_coe {α : Type u_1} [preorder α] {p : α → Prop} {x y : subtype p} :
x y x y
@[simp, norm_cast]
theorem subtype.coe_lt_coe {α : Type u_1} [preorder α] {p : α → Prop} {x y : subtype p} :
x < y x < y
@[protected, instance]
def subtype.partial_order {α : Type u_1} [partial_order α] (p : α → Prop) :
Equations
@[protected, instance]
def subtype.linear_order {α : Type u_1} [linear_order α] (p : α → Prop) :

A subtype of a linear order is a linear order. We explicitly give the proof of decidable equality as the existing instance, in order to not have two instances of decidable equality that are not definitionally equal.

Equations

Pointwise order on α × β #

The lexicographic order is defined in order.lexicographic, and the instances are available via the type synonym α ×ₗ β = α × β.

@[protected, instance]
def prod.has_le (α : Type u) (β : Type v) [has_le α] [has_le β] :
has_le × β)
Equations
theorem prod.le_def {α : Type u} {β : Type v} [has_le α] [has_le β] {x y : α × β} :
x y x.fst y.fst x.snd y.snd
@[simp]
theorem prod.mk_le_mk {α : Type u} {β : Type v} [has_le α] [has_le β] {x₁ x₂ : α} {y₁ y₂ : β} :
(x₁, y₁) (x₂, y₂) x₁ x₂ y₁ y₂
@[protected, instance]
def prod.preorder (α : Type u) (β : Type v) [preorder α] [preorder β] :
preorder × β)
Equations
theorem prod.lt_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {a b : α × β} :
a < b a.fst < b.fst a.snd b.snd a.fst b.fst a.snd < b.snd
@[simp]
theorem prod.mk_lt_mk {α : Type u} {β : Type v} [preorder α] [preorder β] {x₁ x₂ : α} {y₁ y₂ : β} :
(x₁, y₁) < (x₂, y₂) x₁ < x₂ y₁ y₂ x₁ x₂ y₁ < y₂
@[protected, 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 α ×ₗ β = α × β.)

Equations

Additional order classes #

theorem exists_gt {α : Type u} [has_lt α] [no_max_order α] (a : α) :
∃ (a' : α), a < a'
@[protected, instance]
def nonempty_gt {α : Type u} [has_lt α] [no_max_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 roughly an unbundled version of order_bot, except that a preorder may have several top elements. When α is linear, this is useful to make a case disjunction on no_max_order α within a proof.

Equations
@[simp]
theorem not_is_top {α : Type u} [preorder α] [no_max_order α] (a : α) :
theorem is_top.unique {α : Type u} [partial_order α] {a b : α} (ha : is_top a) (hb : a b) :
a = b
theorem is_top_or_exists_gt {α : Type u} [linear_order α] (a : α) :
is_top a ∃ (b : α), a < b
@[class]
structure no_min_order (α : Type u) [has_lt α] :
Prop
  • exists_lt : ∀ (a : α), ∃ (b : α), b < a

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

Instances
theorem exists_lt {α : Type u} [has_lt α] [no_min_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 roughly an unbundled version of order_bot, except that a preorder may have several bottom elements. When α is linear, this is useful to make a case disjunction on no_min_order α within a proof.

Equations
@[simp]
theorem not_is_bot {α : Type u} [preorder α] [no_min_order α] (a : α) :
theorem is_bot.unique {α : Type u} [partial_order α] {a b : α} (ha : is_bot a) (hb : b a) :
a = b
theorem is_bot_or_exists_lt {α : Type u} [linear_order α] (a : α) :
is_bot a ∃ (b : α), b < a
@[protected, instance]
def order_dual.no_max_order (α : Type u) [has_lt α] [no_min_order α] :
@[protected, instance]
def order_dual.no_min_order (α : Type u) [has_lt α] [no_max_order α] :
@[protected, instance]
def nonempty_lt {α : Type u} [has_lt α] [no_min_order α] (a : α) :
nonempty {x // x < a}
theorem exists_between {α : Type u} [has_lt α] [densely_ordered α] {a₁ a₂ : α} :
a₁ < a₂(∃ (a : α), a₁ < a a < a₂)
@[protected, 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
@[protected, instance]
Equations