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 #

order_dual α : A type synonym reversing the meaning of all inequalities.
as_linear_order α: A type synonym to promote partial_order α to linear_order α using is_total α (≤).

Transfering orders #

order.preimage, preorder.lift: Transfers a (pre)order on β to an order on α using a function f : α → β.
partial_order.lift, linear_order.lift: Transfers a partial (resp., linear) order on β to a partial (resp., linear) order on α using an injective function f.

Extra classes #

no_max_order, no_min_order: An order without a maximal/minimal element.
densely_ordered: An order with no gap, i.e. for any two elements a < b there exists c such that a < c < b.

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 #

expand module docs
automatic construction of dual definitions / theorems

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 α) :

x = y ↔ has_le.le = has_le.le

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.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 ≤ 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

@[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 < 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.

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 ≤ 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 α] (hca : c ≤ a) (hbd : b ≤ d) :

a ≤ b → c ≤ d

monotonicity of ≤ with respect to →

@[ext]

theorem preorder.to_has_le_injective {α : Type u_1} :

function.injective (preorder.to_has_le α)

@[ext]

theorem partial_order.to_preorder_injective {α : Type u_1} :

function.injective (partial_order.to_preorder α)

@[ext]

theorem linear_order.to_partial_order_injective {α : Type u_1} :

function.injective (linear_order.to_partial_order α)

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

(f ⁻¹'o s) x y = s (f x) (f y)

@[protected, instance]

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

decidable_rel (f ⁻¹'o s)

The preimage of a decidable order is decidable.

Equations

order.preimage.decidable f s = λ (x y : α), H (f x) (f y)

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

order_dual α = α

@[protected, instance]

def order_dual.nonempty (α : Type u_1) [h : nonempty α] :

nonempty (order_dual α)

@[protected, instance]

def order_dual.subsingleton (α : Type u_1) [h : subsingleton α] :

subsingleton (order_dual α)

@[protected, instance]

def order_dual.has_le (α : Type u_1) [has_le α] :

has_le (order_dual α)

Equations

order_dual.has_le α = {le := λ (x y : α), y ≤ x}

@[protected, instance]

def order_dual.has_lt (α : Type u_1) [has_lt α] :

has_lt (order_dual α)

Equations

order_dual.has_lt α = {lt := λ (x y : α), y < x}

@[protected, instance]

def order_dual.has_zero (α : Type u_1) [has_zero α] :

has_zero (order_dual α)

Equations

order_dual.has_zero α = {zero := 0}

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 α] :

preorder (order_dual α)

Equations

order_dual.preorder α = {le := has_le.le (order_dual.has_le α), lt := has_lt.lt (order_dual.has_lt α), le_refl := _, le_trans := _, lt_iff_le_not_le := _}

@[protected, instance]

def order_dual.partial_order (α : Type u_1) [partial_order α] :

partial_order (order_dual α)

Equations

order_dual.partial_order α = {le := preorder.le (order_dual.preorder α), lt := preorder.lt (order_dual.preorder α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[protected, instance]

def order_dual.linear_order (α : Type u_1) [linear_order α] :

linear_order (order_dual α)

Equations

order_dual.linear_order α = {le := partial_order.le (order_dual.partial_order α), lt := partial_order.lt (order_dual.partial_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := infer_instance (λ (a b : α), has_le.le.decidable b a), decidable_eq := decidable_eq_of_decidable_le infer_instance, decidable_lt := infer_instance (λ (a b : α), has_lt.lt.decidable b a), max := min _inst_1, max_def := _, min := max _inst_1, min_def := _}

@[protected, instance]

def order_dual.inhabited {α : Type u} [inhabited α] :

inhabited (order_dual α)

Equations

order_dual.inhabited = id

theorem order_dual.preorder.dual_dual (α : Type u_1) [H : preorder α] :

order_dual.preorder (order_dual α) = H

theorem order_dual.partial_order.dual_dual (α : Type u_1) [H : partial_order α] :

order_dual.partial_order (order_dual α) = H

theorem order_dual.linear_order.dual_dual (α : Type u_1) [H : linear_order α] :

order_dual.linear_order (order_dual α) = H

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

pi.has_le = {le := λ (x y : Π (i : ι), α i), ∀ (i : ι), x i ≤ y i}

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

pi.preorder = {le := has_le.le pi.has_le, lt := λ (a b : Π (i : ι), α i), a ≤ b ∧ ¬b ≤ a, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

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 ≠ i → x 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 ≠ i → x 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 ≠ i → x j ≤ y j

@[protected, instance]

def pi.partial_order {ι : Type u} {α : ι → Type v} [Π (i : ι), partial_order (α i)] :

partial_order (Π (i : ι), α i)

Equations

pi.partial_order = {le := preorder.le pi.preorder, lt := preorder.lt pi.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

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

preorder.lift f = {le := λ (x y : α), f x ≤ f y, lt := λ (x y : α), f x < f y, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

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

partial_order α

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

Equations

partial_order.lift f inj = {le := preorder.le (preorder.lift f), lt := preorder.lt (preorder.lift f), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

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

linear_order α

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

Equations

linear_order.lift f inj = {le := partial_order.le (partial_order.lift f inj), lt := partial_order.lt (partial_order.lift f inj), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (x y : α), infer_instance, decidable_eq := λ (x y : α), decidable_of_iff (f x = f y) _, decidable_lt := λ (x y : α), infer_instance, max := max_default (λ (a b : α), infer_instance), max_def := _, min := min_default (λ (a b : α), infer_instance), min_def := _}

@[protected, instance]

def subtype.preorder {α : Type u_1} [preorder α] (p : α → Prop) :

preorder (subtype p)

Equations

subtype.preorder p = preorder.lift coe

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

partial_order (subtype p)

Equations

subtype.partial_order p = partial_order.lift coe subtype.coe_injective

@[protected, instance]

def subtype.linear_order {α : Type u_1} [linear_order α] (p : α → Prop) :

linear_order (subtype p)

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

subtype.linear_order p = {le := linear_order.le (linear_order.lift coe subtype.coe_injective), lt := linear_order.lt (linear_order.lift coe subtype.coe_injective), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift coe subtype.coe_injective), decidable_eq := subtype.decidable_eq (λ (a b : α), eq.decidable a b), decidable_lt := linear_order.decidable_lt (linear_order.lift coe subtype.coe_injective), max := max (linear_order.lift coe subtype.coe_injective), max_def := _, min := min (linear_order.lift coe subtype.coe_injective), min_def := _}

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

prod.has_le α β = {le := λ (p q : α × β), p.fst ≤ q.fst ∧ p.snd ≤ q.snd}

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

prod.preorder α β = {le := has_le.le (prod.has_le α β), lt := λ (a b : α × β), a ≤ b ∧ ¬b ≤ a, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

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 β] :

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

prod.partial_order α β = {le := preorder.le (prod.preorder α β), lt := preorder.lt (prod.preorder α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

Additional order classes #

@[class]

structure no_max_order (α : Type u) [has_lt α] :

Prop

exists_gt : ∀ (a : α), ∃ (b : α), a < b

Order without a maximal element. Sometimes called cofinal.

Instances

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

is_top a = ∀ (b : α), b ≤ a

@[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

is_bot a = ∀ (b : α), a ≤ b

@[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 α] :

no_max_order (order_dual α)

@[protected, instance]

def order_dual.no_min_order (α : Type u) [has_lt α] [no_max_order α] :

no_min_order (order_dual α)

@[protected, instance]

def nonempty_lt {α : Type u} [has_lt α] [no_min_order α] (a : α) :

nonempty {x // x < a}

@[class]

structure densely_ordered (α : Type u) [has_lt α] :

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} [has_lt α] [densely_ordered α] {a₁ a₂ : α} :

a₁ < a₂ → (∃ (a : α), a₁ < a ∧ a < a₂)

@[protected, instance]

def order_dual.densely_ordered (α : Type u) [has_lt α] [densely_ordered α] :

densely_ordered (order_dual α)

theorem le_of_forall_le_of_dense {α : Type u} [linear_order α] [densely_ordered α] {a₁ a₂ : α} (h : ∀ (a : α), a₂ < a → a₁ ≤ 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₂ < a → a₁ ≤ 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₁ < a → a₂ ≤ 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

as_linear_order α = α

@[protected, instance]

def as_linear_order.inhabited {α : Type u_1} [inhabited α] :

inhabited (as_linear_order α)

Equations

as_linear_order.inhabited = {default := default _inst_1}

@[protected, instance]

noncomputable def as_linear_order.linear_order {α : Type u_1} [partial_order α] [is_total α has_le.le] :

linear_order (as_linear_order α)

Equations

as_linear_order.linear_order = {le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := classical.dec_rel has_le.le, decidable_eq := decidable_eq_of_decidable_le (classical.dec_rel has_le.le), decidable_lt := decidable_lt_of_decidable_le (classical.dec_rel has_le.le), max := max_default (λ (a b : as_linear_order α), classical.dec_rel has_le.le a b), max_def := _, min := min_default (λ (a b : as_linear_order α), classical.dec_rel has_le.le a b), min_def := _}