Basic definitions about `≤` and `<` #

Definitions #

Predicates on functions #

monotone f: A function between two types equipped with ≤ is monotone if a ≤ b implies f a ≤ f b.
strict_mono f : A function between two types equipped with < is strictly monotone if a < b implies f a < f b.
order_dual α : A type tag reversing the meaning of all inequalities.

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_top_order, no_bot_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.

Main theorems #

monotone_of_monotone_nat: If f : ℕ → α and f n ≤ f (n + 1) for all n, then f is monotone.
strict_mono.nat: If f : ℕ → α and f n < f (n + 1) for all n, then f is strictly monotone.

TODO #

expand module docs
automatic construction of dual definitions / theorems

Tags #

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

source

@[simp]

theorem lt_self_iff_false {α : Type u} [preorder α] (a : α) :

a < a ↔ false

source

theorem has_le.ext {α : Type u} (x y : has_le α) (h : has_le.le = has_le.le) :

x = y

source

theorem has_le.ext_iff {α : Type u} (x y : has_le α) :

x = y ↔ has_le.le = has_le.le

source

@[ext]

theorem preorder.to_has_le_injective {α : Type u_1} :

function.injective (preorder.to_has_le α)

source

@[ext]

theorem partial_order.to_preorder_injective {α : Type u_1} :

function.injective (partial_order.to_preorder α)

source

@[ext]

theorem linear_order.to_partial_order_injective {α : Type u_1} :

function.injective (linear_order.to_partial_order α)

source

theorem preorder.ext {α : Type u_1} {A B : preorder α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

source

theorem partial_order.ext {α : Type u_1} {A B : partial_order α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

source

theorem linear_order.ext {α : Type u_1} {A B : linear_order α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

source

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

source

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

source

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

monotone f = ∀ ⦃a b : α⦄, a ≤ b → f a ≤ f b

source

theorem monotone_id {α : Type u} [preorder α] :

monotone id

source

theorem monotone_const {α : Type u} {β : Type v} [preorder α] [preorder β] {b : β} :

monotone (λ (a : α), b)

source

theorem monotone.comp {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} (m_g : monotone g) (m_f : monotone f) :

monotone (g ∘ f)

source

theorem monotone.iterate {α : Type u} [preorder α] {f : α → α} (hf : monotone f) (n : ℕ) :

monotone f^[n]

source

theorem monotone_of_monotone_nat {α : Type u} [preorder α] {f : ℕ → α} (hf : ∀ (n : ℕ), f n ≤ f (n + 1)) :

monotone f

source

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'

source

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.

source

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.

source

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

strict_mono f = ∀ ⦃a b : α⦄, a < b → f a < f b

source

theorem strict_mono_id {α : Type u} [has_lt α] :

strict_mono id

source

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

strict_mono_incr_on f t = ∀ ⦃x : α⦄, x ∈ t → ∀ ⦃y : α⦄, y ∈ t → x < y → f x < f y

source

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

strict_mono_decr_on f t = ∀ ⦃x : α⦄, x ∈ t → ∀ ⦃y : α⦄, y ∈ t → x < y → f y < f x

source

def order_dual (α : Type u_1) :

Type u_1

Type tag for a set with dual order: ≤ means ≥ and < means >.

Equations

order_dual α = α

source

@[instance]

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

nonempty (order_dual α)

source

@[instance]

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

subsingleton (order_dual α)

source

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

source

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

source

@[instance]

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

has_zero (order_dual α)

Equations

order_dual.has_zero α = {zero := 0}

source

theorem order_dual.dual_le {α : Type u} [has_le α] {a b : α} :

a ≤ b ↔ b ≤ a

source

theorem order_dual.dual_lt {α : Type u} [has_lt α] {a b : α} :

a < b ↔ b < a

source

theorem order_dual.dual_compares {α : Type u} [has_lt α] {a b : α} {o : ordering} :

o.compares a b ↔ o.compares b a

source

@[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 := _}

source

@[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 := _}

source

@[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 := (λ (this : decidable_rel (λ (a b : α), b ≤ a)), this) (λ (a b : α), has_le.le.decidable b a), decidable_eq := decidable_eq_of_decidable_le ((λ (this : decidable_rel (λ (a b : α), b ≤ a)), this) (λ (a b : α), has_le.le.decidable b a)), decidable_lt := (λ (this : decidable_rel (λ (a b : α), b < a)), this) (λ (a b : α), has_lt.lt.decidable b a)}

source

@[instance]

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

inhabited (order_dual α)

Equations

order_dual.inhabited = id

source

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

order_dual.preorder (order_dual α) = H

source

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

order_dual.partial_order (order_dual α) = H

source

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

order_dual.linear_order (order_dual α) = H

source

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

source

theorem strict_mono_incr_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (H : strict_mono_incr_on f s) :

strict_mono_incr_on f s

source

theorem strict_mono_incr_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (H : strict_mono_incr_on f s) :

strict_mono_decr_on f s

source

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

source

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

source

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

source

theorem strict_mono_decr_on.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (H : strict_mono_decr_on f s) :

strict_mono_decr_on f s

source

theorem strict_mono_decr_on.dual_right {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s : set α} (H : strict_mono_decr_on f s) :

strict_mono_incr_on f s

source

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

source

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

source

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

source

theorem strict_mono.strict_mono_incr_on {α : Type u} {β : Type v} [has_lt α] [has_lt β] {f : α → β} (hf : strict_mono f) (s : set α) :

strict_mono_incr_on f s

source

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

strict_mono (g ∘ f)

source

theorem strict_mono.iterate {α : Type u} [has_lt α] {f : α → α} (hf : strict_mono f) (n : ℕ) :

strict_mono f^[n]

source

theorem strict_mono.id_le {φ : ℕ → ℕ} (h : strict_mono φ) (n : ℕ) :

n ≤ φ n

source

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 < y → p y → p x) (hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y) :

strict_mono (λ (x : α), ite (p x) (f x) (g x))

source

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 < y → p y → p x) (hfg : ∀ (x : α), f x ≤ g x) :

strict_mono (λ (x : α), ite (p x) (f x) (g x))

source

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

source

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

source

theorem strict_mono.injective {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} (H : strict_mono f) :

function.injective f

source

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

source

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

source

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

source

theorem strict_mono.nat {β : Type u_1} [preorder β] {f : ℕ → β} (h : ∀ (n : ℕ), f n < f (n + 1)) :

strict_mono f

source

theorem strict_mono.monotone {α : Type u} {β : Type v} [partial_order α] [preorder β] {f : α → β} (H : strict_mono f) :

monotone f

source

theorem injective_of_lt_imp_ne {α : Type u} {β : Type v} [linear_order α] {f : α → β} (h : ∀ (x y : α), x < y → f x ≠ f y) :

function.injective f

source

theorem injective_of_le_imp_le {α : Type u} {β : Type v} [partial_order α] [preorder β] (f : α → β) (h : ∀ {x y : α}, f x ≤ f y → x ≤ y) :

function.injective f

source

theorem strict_mono_of_monotone_of_injective {α : Type u} {β : Type v} [partial_order α] [partial_order β] {f : α → β} (h₁ : monotone f) (h₂ : function.injective f) :

strict_mono f

source

theorem monotone.strict_mono_iff_injective {α : Type u} {β : Type v} [linear_order α] [partial_order β] {f : α → β} (h : monotone f) :

strict_mono f ↔ function.injective f

source

theorem strict_mono_of_le_iff_le {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (h : ∀ (x y : α), x ≤ y ↔ f x ≤ f y) :

strict_mono f

Order instances on the function space #

source

@[instance]

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

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

Equations

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

source

theorem pi.le_def {ι : Type u} {α : ι → Type v} [Π (i : ι), preorder (α i)] {x y : Π (i : ι), α i} :

x ≤ y ↔ ∀ (i : ι), x i ≤ y i

source

theorem pi.lt_def {ι : Type u} {α : ι → Type v} [Π (i : ι), preorder (α i)] {x y : Π (i : ι), α i} :

x < y ↔ x ≤ y ∧ ∃ (i : ι), x i < y i

source

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

source

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

source

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

source

@[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 := _}

source

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

source

theorem monotone.order_dual {α : Type u} {γ : Type w} [preorder α] [preorder γ] {f : α → γ} (hf : monotone f) :

monotone f

source

theorem monotone_lam {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] {f : α → β → γ} (m : ∀ (b : β), monotone (λ (a : α), f a b)) :

monotone f

source

theorem monotone_app {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder γ] (f : β → α → γ) (b : β) (m : monotone (λ (a : α) (b : β), f b a)) :

monotone (f b)

source

theorem strict_mono.order_dual {α : Type u} {β : Type v} [has_lt α] [has_lt β] {f : α → β} (hf : strict_mono f) :

strict_mono f

source

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

preorder α

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 := _}

source

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 := _}

source

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}

source

@[instance]

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

preorder (subtype p)

Equations

subtype.preorder p = preorder.lift subtype.val

source

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

source

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

source

@[simp]

theorem subtype.coe_le_coe {α : Type u_1} [preorder α] {p : α → Prop} {x y : subtype p} :

↑x ≤ ↑y ↔ x ≤ y

source

@[simp]

theorem subtype.coe_lt_coe {α : Type u_1} [preorder α] {p : α → Prop} {x y : subtype p} :

↑x < ↑y ↔ x < y

source

@[instance]

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

partial_order (subtype p)

Equations

subtype.partial_order p = partial_order.lift subtype.val subtype.val_injective

source

@[instance]

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

linear_order (subtype p)

Equations

subtype.linear_order p = linear_order.lift subtype.val subtype.val_injective

source

theorem subtype.mono_coe {α : Type u} [preorder α] (t : set α) :

monotone coe

source

theorem subtype.strict_mono_coe {α : Type u} [preorder α] (t : set α) :

strict_mono coe

source

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

source

@[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 := _}

source

@[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 lex α β = α × β.)

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 #

source

@[class]

structure no_top_order (α : Type u) [preorder α] :

Prop

no_top : ∀ (a : α), ∃ (a' : α), a < a'

order without a top element; sometimes called cofinal

Instances

source

theorem no_top {α : Type u} [preorder α] [no_top_order α] (a : α) :

∃ (a' : α), a < a'

source

@[instance]

def nonempty_gt {α : Type u} [preorder α] [no_top_order α] (a : α) :

nonempty {x // a < x}

source

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

source

theorem no_bot {α : Type u} [preorder α] [no_bot_order α] (a : α) :

∃ (a' : α), a' < a

source

@[instance]

def order_dual.no_top_order (α : Type u) [preorder α] [no_bot_order α] :

no_top_order (order_dual α)

source

@[instance]

def order_dual.no_bot_order (α : Type u) [preorder α] [no_top_order α] :

no_bot_order (order_dual α)

source

@[instance]

def nonempty_lt {α : Type u} [preorder α] [no_bot_order α] (a : α) :

nonempty {x // x < a}

source

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

source

theorem exists_between {α : Type u} [preorder α] [densely_ordered α] {a₁ a₂ : α} :

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

source

@[instance]

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

densely_ordered (order_dual α)

source

theorem le_of_forall_le_of_dense {α : Type u} [linear_order α] [densely_ordered α] {a₁ a₂ : α} (h : ∀ (a : α), a₂ < a → a₁ ≤ a) :

a₁ ≤ a₂

source

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₂

source

theorem le_of_forall_ge_of_dense {α : Type u} [linear_order α] [densely_ordered α] {a₁ a₂ : α} (h : ∀ (a₃ : α), a₃ < a₁ → a₃ ≤ a₂) :

a₁ ≤ a₂

source

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₂

source

theorem dense_or_discrete {α : Type u} [linear_order α] (a₁ a₂ : α) :