mathlib documentation

order.basic

Basic definitions about and < #

Definitions #

Predicates on functions #

Transfering orders #

Extra classes #

Main theorems #

TODO #

See also #

Tags #

preorder, order, partial order, linear order, monotone, strictly monotone

@[simp]
theorem lt_self_iff_false {α : Type u} [preorder α] (a : α) :
a < a false
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 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
def monotone {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α → β) :
Prop

A function between preorders is monotone if a ≤ b implies f a ≤ f b.

Equations
theorem monotone_id {α : Type u} [preorder α] :
theorem monotone_const {α : Type u} {β : Type v} [preorder α] [preorder β] {b : β} :
monotone (λ (a : α), b)
theorem monotone.comp {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} (m_g : monotone g) (m_f : monotone f) :
theorem monotone.iterate {α : Type u} [preorder α] {f : α → α} (hf : monotone f) (n : ) :
theorem monotone_of_monotone_nat {α : Type u} [preorder α] {f : → α} (hf : ∀ (n : ), f n f (n + 1)) :
theorem monotone.reflect_lt {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {f : α → β} (hf : monotone f) {x x' : α} (h : f x < f x') :
x < x'
theorem monotone.ne_of_lt_of_lt_nat {α : Type u_1} [preorder α] {f : → α} (hf : monotone f) (x x' : ) {y : α} (h1 : f x < y) (h2 : y < f (x + 1)) :
f x' y

If f is a monotone function from to a preorder such that y lies between f x and f (x + 1), then y doesn't lie in the range of f.

theorem monotone.ne_of_lt_of_lt_int {α : Type u_1} [preorder α] {f : → α} (hf : monotone f) (x x' : ) {y : α} (h1 : f x < y) (h2 : y < f (x + 1)) :
f x' y

If f is a monotone function from to a preorder such that y lies between f x and f (x + 1), then y doesn't lie in the range of f.

def strict_mono {α : Type u} {β : Type v} [has_lt α] [has_lt β] (f : α → β) :
Prop

A function f is strictly monotone if a < b implies f a < f b.

Equations
theorem strict_mono_id {α : Type u} [has_lt α] :
def strict_mono_incr_on {α : Type u} {β : Type v} [has_lt α] [has_lt β] (f : α → β) (t : set α) :
Prop

A function f is strictly monotone increasing on t if x < y for x,y ∈ t implies f x < f y.

Equations
def strict_mono_decr_on {α : Type u} {β : Type v} [has_lt α] [has_lt β] (f : α → β) (t : set α) :
Prop

A function f is strictly monotone decreasing on t if x < y for x,y ∈ t implies f y < f x.

Equations
def order_dual (α : Type u_1) :
Type u_1

Type tag for a set with 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
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
theorem order_dual.dual_compares {α : Type u} [has_lt α] {a b : α} {o : ordering} :
o.compares a b o.compares b a
@[instance]
def order_dual.preorder (α : Type u_1) [preorder α] :
Equations
@[instance]
def order_dual.linear_order (α : Type u_1) [linear_order α] :
Equations
@[instance]
def order_dual.inhabited {α : Type u} [inhabited α] :
Equations
theorem order_dual.preorder.dual_dual (α : Type u_1) [H : preorder α] :
theorem order_dual.cmp_le_flip {α : Type u_1} [has_le α] [decidable_rel has_le.le] (x y : α) :
cmp_le x y = cmp_le y x
theorem strict_mono_incr_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (H : strict_mono_incr_on f s) :
theorem strict_mono_incr_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (H : strict_mono_incr_on f s) :
theorem strict_mono_incr_on.le_iff_le {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} {x y : α} (H : strict_mono_incr_on f s) (hx : x s) (hy : y s) :
f x f y x y
theorem strict_mono_incr_on.lt_iff_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} {x y : α} (H : strict_mono_incr_on f s) (hx : x s) (hy : y s) :
f x < f y x < y
theorem strict_mono_incr_on.compares {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} {x y : α} (H : strict_mono_incr_on f s) (hx : x s) (hy : y s) {o : ordering} :
o.compares (f x) (f y) o.compares x y
theorem strict_mono_decr_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (H : strict_mono_decr_on f s) :
theorem strict_mono_decr_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (H : strict_mono_decr_on f s) :
theorem strict_mono_decr_on.le_iff_le {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} {x y : α} (H : strict_mono_decr_on f s) (hx : x s) (hy : y s) :
f x f y y x
theorem strict_mono_decr_on.lt_iff_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} {x y : α} (H : strict_mono_decr_on f s) (hx : x s) (hy : y s) :
f x < f y y < x
theorem strict_mono_decr_on.compares {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} {x y : α} (H : strict_mono_decr_on f s) (hx : x s) (hy : y s) {o : ordering} :
o.compares (f x) (f y) o.compares y x
theorem strict_mono.strict_mono_incr_on {α : Type u} {β : Type v} [has_lt α] [has_lt β] {f : α → β} (hf : strict_mono f) (s : set α) :
theorem strict_mono.comp {α : Type u} {β : Type v} {γ : Type w} [has_lt α] [has_lt β] [has_lt γ] {g : β → γ} {f : α → β} (hg : strict_mono g) (hf : strict_mono f) :
theorem strict_mono.iterate {α : Type u} [has_lt α] {f : α → α} (hf : strict_mono f) (n : ) :
theorem strict_mono.id_le {φ : } (h : strict_mono φ) (n : ) :
n φ n
theorem strict_mono.ite' {α : Type u} {β : Type v} [preorder α] [has_lt β] {f g : α → β} (hf : strict_mono f) (hg : strict_mono g) {p : α → Prop} [decidable_pred p] (hp : ∀ ⦃x y : α⦄, x < yp yp x) (hfg : ∀ ⦃x y : α⦄, p x¬p yx < yf x < g y) :
strict_mono (λ (x : α), ite (p x) (f x) (g x))
theorem strict_mono.ite {α : Type u} {β : Type v} [preorder α] [preorder β] {f g : α → β} (hf : strict_mono f) (hg : strict_mono g) {p : α → Prop} [decidable_pred p] (hp : ∀ ⦃x y : α⦄, x < yp yp x) (hfg : ∀ (x : α), f x g x) :
strict_mono (λ (x : α), ite (p x) (f x) (g x))
theorem strict_mono.lt_iff_lt {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (H : strict_mono f) {a b : α} :
f a < f b a < b
theorem strict_mono.compares {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (H : strict_mono f) {a b : α} {o : ordering} :
o.compares (f a) (f b) o.compares a b
theorem strict_mono.injective {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (H : strict_mono f) :
theorem strict_mono.le_iff_le {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (H : strict_mono f) {a b : α} :
f a f b a b
theorem strict_mono.top_preimage_top {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (H : strict_mono f) {a : α} (h_top : ∀ (p : β), p f a) (x : α) :
x a
theorem strict_mono.bot_preimage_bot {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (H : strict_mono f) {a : α} (h_bot : ∀ (p : β), f a p) (x : α) :
a x
theorem strict_mono.nat {β : Type u_1} [preorder β] {f : → β} (h : ∀ (n : ), f n < f (n + 1)) :
theorem strict_mono.monotone {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} (H : strict_mono f) :
theorem injective_of_lt_imp_ne {α : Type u} {β : Type v} [linear_order α] {f : α → β} (h : ∀ (x y : α), x < yf x f y) :
theorem strict_mono_of_monotone_of_injective {α : Type u} {β : Type v} [partial_order α] [partial_order β] {f : α → β} (h₁ : monotone f) (h₂ : function.injective f) :
theorem monotone.strict_mono_iff_injective {α : Type u} {β : Type v} [linear_order α] [partial_order β] {f : α → β} (h : monotone f) :
theorem strict_mono_of_le_iff_le {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (h : ∀ (x y : α), x y f x f y) :

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
theorem comp_le_comp_left_of_monotone {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] {f : β → α} {g h : γ → β} (m_f : monotone f) (le_gh : g h) :
f g f h
theorem monotone.order_dual {α : Type u} {γ : Type w} [preorder α] [preorder γ] {f : α → γ} (hf : monotone f) :
theorem monotone_lam {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] {f : α → β → γ} (m : ∀ (b : β), monotone (λ (a : α), f a b)) :
theorem monotone_app {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] (f : β → α → γ) (b : β) (m : monotone (λ (a : α) (b : β), f b a)) :
monotone (f b)
theorem strict_mono.order_dual {α : Type u} {β : Type v} [has_lt α] [has_lt β] {f : α → β} (hf : strict_mono f) :
def preorder.lift {α : Type u_1} {β : Type u_2} [preorder β] (f : α → β) :

Transfer a preorder on β to a preorder on α using a function f : α → β.

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 : α → β.

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 : α → β.

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
theorem subtype.mono_coe {α : Type u} [preorder α] (t : set α) :
theorem subtype.strict_mono_coe {α : Type u} [preorder α] (t : set α) :
@[instance]
def prod.has_le (α : Type u) (β : Type v) [has_le α] [has_le β] :
has_le × β)
Equations
@[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 top element; somtimes 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}
@[class]
structure no_bot_order (α : Type u) [preorder α] :
Prop
  • no_bot : ∀ (a : α), ∃ (a' : α), a' < a

order without a bottom element; somtimes called coinitial or dense

Instances
theorem no_bot {α : Type u} [preorder α] [no_bot_order α] (a : α) :
∃ (a' : α), a' < a
@[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₃ > 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₁
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