Basic definitions about ≤ and <
Definitions
Predicates on functions
monotone f: a function between two types equipped with≤is monotone ifa ≤ bimpliesf a ≤ f b.strict_mono f: a function between two types equipped with<is strictly monotone ifa < bimpliesf a < f b.order_dual α: a type tag reversing the meaning of all inequalities.
Transfering orders
order.preimage,preorder.lift: transfer a (pre)order onβto an order onαusing a functionf : α → β.partial_order.lift,linear_order.lift,decidable_linear_order.lift: transfer a partial (resp., linear, decidable linear) order onβto a partial (resp., linear, decidable linear) order onαusing an injective functionf.
Extra classes
no_top_order,no_bot_order: an order without a maximal/minimal element.densely_ordered: an order with no gaps, i.e. for any two elementsa<bthere existsc,a<c<b.
Main theorems
monotone_of_monotone_nat: iff : ℕ → αandf n ≤ f (n + 1)for alln, thenfis monotone;strict_mono.nat: iff : ℕ → αandf n < f (n + 1)for alln, then f is strictly monotone.
TODO
- expand module docs
- automatic construction of dual definitions / theorems
See also
algebra.orderfor basic lemmas about orders, and projection notation for orders
Tags
preorder, order, partial order, linear order, monotone, strictly monotone
@[simp]
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).
@[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)
theorem
monotone_const
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{b : β} :
monotone (λ (a : α), b)
theorem
reflect_lt
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[preorder β]
{f : α → β}
(hf : monotone f)
{x x' : α} :
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
theorem
strict_mono.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[has_lt α]
[has_lt β]
[has_lt γ]
{g : β → γ}
{f : α → β} :
strict_mono g → strict_mono f → strict_mono (g ∘ f)
theorem
strict_mono.lt_iff_lt
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(H : strict_mono f)
{a b : α} :
theorem
strict_mono.injective
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β} :
theorem
strict_mono.compares
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(H : strict_mono f)
{a b : α}
{o : ordering} :
theorem
strict_mono.le_iff_le
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
(H : strict_mono f)
{a b : α} :
theorem
strict_mono.nat
{β : Type u_1}
[preorder β]
{f : ℕ → β} :
(∀ (n : ℕ), f n < f (n + 1)) → strict_mono f
theorem
strict_mono.monotone
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
{f : α → β} :
strict_mono f → monotone f
theorem
injective_of_lt_imp_ne
{α : Type u}
{β : Type v}
[linear_order α]
{f : α → β} :
(∀ (x y : α), x < y → f x ≠ f y) → function.injective f
theorem
strict_mono_of_monotone_of_injective
{α : Type u}
{β : Type v}
[partial_order α]
[partial_order β]
{f : α → β} :
monotone f → function.injective f → strict_mono f
theorem
strict_mono_of_le_iff_le
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β} :
(∀ (x y : α), x ≤ y ↔ f x ≤ f y) → strict_mono f
Type tag for a set with dual order: ≤ means ≥ and < means >.
Equations
- order_dual α = α
@[instance]
Equations
- _ = h
@[instance]
Equations
- order_dual.has_le α = {le := λ (x y : α), y ≤ x}
@[instance]
Equations
- order_dual.has_lt α = {lt := λ (x y : α), y < x}
@[instance]
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 := _}
@[instance]
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 := _}
@[instance]
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 := _}
@[instance]
Equations
- order_dual.decidable_linear_order α = {le := linear_order.le (order_dual.linear_order α), lt := linear_order.lt (order_dual.linear_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)}
@[instance]
Equations
@[instance]
def
pi.preorder
{ι : Type u}
{α : ι → Type v}
[Π (i : ι), preorder (α i)] :
preorder (Π (i : ι), α i)
@[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 := _}
theorem
strict_mono.order_dual
{α : Type u}
{β : Type v}
[has_lt α]
[has_lt β]
{f : α → β} :
strict_mono f → strict_mono f
Transfer a partial_order on β to a partial_order on α using an injective
function f : α → β.
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 := _}
Transfer a linear_order on β to a linear_order on α using an injective
function f : α → β.
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 := _}
def
decidable_linear_order.lift
{α : Type u_1}
{β : Type u_2}
[decidable_linear_order β]
(f : α → β) :
Transfer a decidable_linear_order on β to a decidable_linear_order on α using
an injective function f : α → β.
Equations
- decidable_linear_order.lift f inj = {le := linear_order.le (linear_order.lift f inj), lt := linear_order.lt (linear_order.lift f inj), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (x y : α), show decidable (f x ≤ f y), from has_le.le.decidable (f x) (f y), decidable_eq := λ (x y : α), decidable_of_iff (f x = f y) _, decidable_lt := λ (x y : α), show decidable (f x < f y), from has_lt.lt.decidable (f x) (f y)}
@[instance]
Equations
@[instance]
def
subtype.partial_order
{α : Type u_1}
[partial_order α]
(p : α → Prop) :
partial_order (subtype p)
@[instance]
@[instance]
@[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
@[class]
- no_top : ∀ (a : α), ∃ (a' : α), a < a'
order without a top element; somtimes called cofinal
@[instance]
Equations
- _ = _
@[class]
- no_bot : ∀ (a : α), ∃ (a' : α), a' < a
order without a bottom element; somtimes called coinitial or dense
@[instance]
Equations
- _ = _
@[instance]
Equations
- _ = _
@[instance]
Equations
- _ = _
@[class]
An order is dense if there is an element between any pair of distinct elements.
@[instance]
Equations
- _ = _
theorem
eq_of_le_of_forall_le_of_dense
{α : Type u}
[linear_order α]
[densely_ordered α]
{a₁ a₂ : α} :
theorem
eq_of_le_of_forall_ge_of_dense
{α : Type u}
[linear_order α]
[densely_ordered α]
{a₁ a₂ : α} :
Any linear_order is a noncomputable decidable_linear_order. This is not marked
as an instance to avoid a loop.
Equations
- classical.DLO α = {le := linear_order.le LO, lt := linear_order.lt LO, 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)}