order.basic

Basic definitions about `≤` and `<`#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, with notation `αᵒᵈ`.
• `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 class #

• `has_sup`: type class for the `⊔` notation
• `has_inf`: type class for the `⊓` notation
• `has_compl`: type class for the `ᶜ` notation
• `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 le_trans' {α : Type u} [preorder α] {a b c : α} :
b c a b a c
theorem lt_trans' {α : Type u} [preorder α] {a b c : α} :
b < c a < b a < c
theorem lt_of_le_of_lt' {α : Type u} [preorder α] {a b c : α} :
b c a < b a < c
theorem lt_of_lt_of_le' {α : Type u} [preorder α] {a b c : α} :
b < c a b a < c
theorem ge_antisymm {α : Type u} {a b : α} :
a b b a b = a
theorem lt_of_le_of_ne' {α : Type u} {a b : α} :
a b b a a < b
theorem ne.lt_of_le {α : Type u} {a b : α} :
a b a b a < b
theorem ne.lt_of_le' {α : Type u} {a b : α} :
b a a b a < b
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
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' {α : Type u} [preorder α] {a b c : α} :
b c a b 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.trans_lt' {α : Type u} [preorder α] {a b c : α} :
b c a < b a < c

Alias of `lt_of_le_of_lt'`.

theorem has_le.le.antisymm {α : Type u} {a b : α} :
a b b a a = b

Alias of `le_antisymm`.

theorem has_le.le.antisymm' {α : Type u} {a b : α} :
a b b a b = a

Alias of `ge_antisymm`.

theorem has_le.le.lt_of_ne {α : Type u} {a b : α} :
a b a b a < b

Alias of `lt_of_le_of_ne`.

theorem has_le.le.lt_of_ne' {α : Type u} {a b : α} :
a b b a 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} {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} {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' {α : Type u} [preorder α] {a b c : α} :
b < c a < b 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.trans_le' {α : Type u} [preorder α] {a b c : α} :
b < c a b 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 α] {a : α} :
a a

A version of `le_refl` where the argument is implicit

@[simp]
theorem lt_self_iff_false {α : Type u} [preorder α] (x : α) :
x < x false
theorem le_of_le_of_eq {α : Type u} [preorder α] {a b c : α} (hab : a b) (hbc : b = c) :
a c
theorem le_of_eq_of_le {α : Type u} [preorder α] {a b c : α} (hab : a = b) (hbc : b c) :
a c
theorem lt_of_lt_of_eq {α : Type u} [preorder α] {a b c : α} (hab : a < b) (hbc : b = c) :
a < c
theorem lt_of_eq_of_lt {α : Type u} [preorder α] {a b c : α} (hab : a = b) (hbc : b < c) :
a < c
theorem le_of_le_of_eq' {α : Type u} [preorder α] {a b c : α} :
b c a = b a c
theorem le_of_eq_of_le' {α : Type u} [preorder α] {a b c : α} :
b = c a b a c
theorem lt_of_lt_of_eq' {α : Type u} [preorder α] {a b c : α} :
b < c a = b a < c
theorem lt_of_eq_of_lt' {α : Type u} [preorder α] {a b c : α} :
b = c a < b a < c
theorem has_le.le.trans_eq {α : Type u} [preorder α] {a b c : α} (hab : a b) (hbc : b = c) :
a c

Alias of `le_of_le_of_eq`.

theorem has_le.le.trans_eq' {α : Type u} [preorder α] {a b c : α} :
b c a = b a c

Alias of `le_of_le_of_eq'`.

theorem has_lt.lt.trans_eq {α : Type u} [preorder α] {a b c : α} (hab : a < b) (hbc : b = c) :
a < c

Alias of `lt_of_lt_of_eq`.

theorem has_lt.lt.trans_eq' {α : Type u} [preorder α] {a b c : α} :
b < c a = b a < c

Alias of `lt_of_lt_of_eq'`.

theorem eq.trans_le {α : Type u} [preorder α] {a b c : α} (hab : a = b) (hbc : b c) :
a c

Alias of `le_of_eq_of_le`.

theorem eq.trans_ge {α : Type u} [preorder α] {a b c : α} :
b = c a b a c

Alias of `le_of_eq_of_le'`.

theorem eq.trans_lt {α : Type u} [preorder α] {a b c : α} (hab : a = b) (hbc : b < c) :
a < c

Alias of `lt_of_eq_of_lt`.

theorem eq.trans_gt {α : Type u} [preorder α] {a b c : α} :
b = c a < b a < c

Alias of `lt_of_eq_of_lt'`.

@[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.not_lt {α : Type u} [preorder α] {x y : α} (h : x = y) :
¬x < y
theorem eq.not_gt {α : Type u} [preorder α] {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.lt_iff_ne {α : Type u} {a b : α} (h : a b) :
a < b a b
theorem has_le.le.gt_iff_ne {α : Type u} {a b : α} (h : a b) :
a < b b a
theorem has_le.le.not_lt_iff_eq {α : Type u} {a b : α} (h : a b) :
¬a < b a = b
theorem has_le.le.not_gt_iff_eq {α : Type u} {a b : α} (h : a b) :
¬a < b b = a
theorem has_le.le.le_iff_eq {α : Type u} {a b : α} (h : a b) :
b a b = a
theorem has_le.le.ge_iff_eq {α : Type u} {a b : α} (h : a b) :
b a a = b
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} [has_le α] {a b : α} :
a b b a
@[simp, nolint]
theorem gt_iff_lt {α : Type u} [has_lt α] {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} {a b : α} :
a b a = b a < b
theorem le_iff_eq_or_lt {α : Type u} {a b : α} :
a b a = b a < b
theorem lt_iff_le_and_ne {α : Type u} {a b : α} :
a < b a b a b
theorem eq_iff_not_lt_of_le {α : Type u_1} {x y : α} :
x y y = x ¬x < y
@[protected]
theorem decidable.eq_iff_le_not_lt {α : Type u} {a b : α} :
a = b a b ¬a < b
theorem eq_iff_le_not_lt {α : Type u} {a b : α} :
a = b a b ¬a < b
theorem eq_or_lt_of_le {α : Type u} {a b : α} (h : a b) :
a = b a < b
theorem eq_or_gt_of_le {α : Type u} {a b : α} (h : a b) :
b = a a < b
theorem gt_or_eq_of_le {α : Type u} {a b : α} (hab : a b) :
a < b b = a
@[nolint]
theorem has_le.le.eq_or_lt_dec {α : Type u} {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} {a b : α} (h : a b) :
a = b a < b

Alias of `eq_or_lt_of_le`.

theorem has_le.le.eq_or_gt {α : Type u} {a b : α} (h : a b) :
b = a a < b

Alias of `eq_or_gt_of_le`.

theorem has_le.le.gt_or_eq {α : Type u} {a b : α} (hab : a b) :
a < b b = a

Alias of `gt_or_eq_of_le`.

theorem eq_of_le_of_not_lt {α : Type u} {a b : α} (hab : a b) (hba : ¬a < b) :
a = b
theorem eq_of_ge_of_not_gt {α : Type u} {a b : α} (hab : a b) (hba : ¬a < b) :
b = a
theorem has_le.le.eq_of_not_lt {α : Type u} {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} {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} {a b : α} (h : a b) :
a b a < b
theorem ne.not_le_or_not_le {α : Type u} {a b : α} (h : a b) :
¬a b ¬b a
@[protected]
theorem decidable.ne_iff_lt_iff_le {α : Type u} [decidable_eq α] {a b : α} :
a b a < b a b
@[simp]
theorem ne_iff_lt_iff_le {α : Type u} {a b : α} :
a b a < b a b
theorem min_def' {α : Type u} [linear_order α] (a b : α) :
= ite (b a) b a
theorem max_def' {α : Type u} [linear_order α] (a b : α) :
= ite (b a) a b
theorem lt_of_not_le {α : Type u} [linear_order α] {a b : α} (h : ¬b a) :
a < b
theorem lt_iff_not_le {α : 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} {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} {a b : α} (H : (c : α), a c b c) :
a = b
theorem eq_of_forall_lt_iff {α : Type u} [linear_order α] {a b : α} (h : (c : α), c < a c < b) :
a = b
theorem eq_of_forall_gt_iff {α : Type u} [linear_order α] {a b : α} (h : (c : α), a < c b < c) :
a = b
theorem rel_imp_eq_of_rel_imp_le {α : Type u} {β : Type v} (r : α α Prop) [ r] {f : α β} (h : (a b : α), r a b f a f b) {a b : α} :
r a b f a = f b

A symmetric relation implies two values are equal, when it implies they're less-equal.

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 `→`

theorem commutative_of_le {α : Type u} {β : Type v} {f : β β α} (comm : (a b : β), f a b f b a) (a b : β) :
f a b = f b a

To prove commutativity of a binary operation `○`, we only to check `a ○ b ≤ b ○ a` for all `a`, `b`.

theorem associative_of_commutative_of_le {α : Type u} {f : α α α} (comm : commutative f) (assoc : (a b c : α), f (f a b) c f a (f b c)) :

To prove associativity of a commutative binary operation `○`, we only to check `(a ○ b) ○ c ≤ a ○ (b ○ c)` for all `a`, `b`, `c`.

@[ext]
theorem preorder.to_has_le_injective {α : Type u_1} :
@[ext]
@[ext]
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
Instances for `order.preimage`
@[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
• = λ (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 `>`. `αᵒᵈ` is notation for `order_dual α`.

Equations
Instances for `order_dual`
@[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
• = {lt := λ (x y : α), y < x}
@[protected, instance]
def order_dual.preorder (α : Type u_1) [preorder α] :
Equations
@[protected, instance]
def order_dual.partial_order (α : Type u_1)  :
Equations
@[protected, instance]
def order_dual.linear_order (α : Type u_1) [linear_order α] :
Equations
@[protected, instance]
def order_dual.inhabited {α : Type u} [inhabited α] :
Equations
theorem order_dual.preorder.dual_dual (α : Type u_1) [H : preorder α] :

`has_compl`#

@[class]
structure has_compl (α : Type u_3) :
Type u_3
• compl : α α

Set / lattice complement

Instances of this typeclass
Instances of other typeclasses for `has_compl`
• has_compl.has_sizeof_inst
@[protected, instance]
def Prop.has_compl  :
Equations
@[protected, instance]
def pi.has_compl {ι : Type u} {α : ι Type v} [Π (i : ι), has_compl (α i)] :
has_compl (Π (i : ι), α i)
Equations
theorem pi.compl_def {ι : Type u} {α : ι Type v} [Π (i : ι), has_compl (α i)] (x : Π (i : ι), α i) :
x = λ (i : ι), (x i)
@[simp]
theorem pi.compl_apply {ι : Type u} {α : ι Type v} [Π (i : ι), has_compl (α i)] (x : Π (i : ι), α i) (i : ι) :
x i = (x i)
@[protected, instance]
def is_irrefl.compl {α : Type u} (r : α α Prop) [ r] :
r
@[protected, instance]
def is_refl.compl {α : Type u} (r : α α Prop) [ r] :
r

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
@[protected, instance]
def pi.partial_order {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), partial_order (π i)] :
partial_order (Π (i : ι), π i)
Equations
def strong_lt {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), has_lt (π i)] (a b : Π (i : ι), π i) :
Prop

A function `a` is strongly less than a function `b` if `a i < b i` for all `i`.

Equations
• b = (i : ι), a i < b i
theorem le_of_strong_lt {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), preorder (π i)] {a b : Π (i : ι), π i} (h : b) :
a b
theorem lt_of_strong_lt {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), preorder (π i)] {a b : Π (i : ι), π i} [nonempty ι] (h : b) :
a < b
theorem strong_lt_of_strong_lt_of_le {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), preorder (π i)] {a b c : Π (i : ι), π i} (hab : b) (hbc : b c) :
c
theorem strong_lt_of_le_of_strong_lt {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), preorder (π i)] {a b c : Π (i : ι), π i} (hab : a b) (hbc : c) :
c
theorem strong_lt.le {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), preorder (π i)] {a b : Π (i : ι), π i} (h : b) :
a b

Alias of `le_of_strong_lt`.

theorem strong_lt.lt {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), preorder (π i)] {a b : Π (i : ι), π i} [nonempty ι] (h : b) :
a < b

Alias of `lt_of_strong_lt`.

theorem strong_lt.trans_le {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), preorder (π i)] {a b c : Π (i : ι), π i} (hab : b) (hbc : b c) :
c

Alias of `strong_lt_of_strong_lt_of_le`.

theorem has_le.le.trans_strong_lt {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), preorder (π i)] {a b c : Π (i : ι), π i} (hab : a b) (hbc : c) :
c

Alias of `strong_lt_of_le_of_strong_lt`.

theorem le_update_iff {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (π i)] {x y : Π (i : ι), π i} {i : ι} {a : π i} :
x a x i a (j : ι), j i x j y j
theorem update_le_iff {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (π i)] {x y : Π (i : ι), π i} {i : ι} {a : π i} :
a y a y i (j : ι), j i x j y j
theorem update_le_update_iff {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (π i)] {x y : Π (i : ι), π i} {i : ι} {a b : π i} :
a b a b (j : ι), j i x j y j
@[simp]
theorem update_le_update_iff' {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (π i)] {x : Π (i : ι), π i} {i : ι} {a b : π i} :
a b a b
@[simp]
theorem update_lt_update_iff {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (π i)] {x : Π (i : ι), π i} {i : ι} {a b : π i} :
a < b a < b
@[simp]
theorem le_update_self_iff {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (π i)] {x : Π (i : ι), π i} {i : ι} {a : π i} :
x a x i a
@[simp]
theorem update_le_self_iff {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (π i)] {x : Π (i : ι), π i} {i : ι} {a : π i} :
a x a x i
@[simp]
theorem lt_update_self_iff {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (π i)] {x : Π (i : ι), π i} {i : ι} {a : π i} :
x < a x i < a
@[simp]
theorem update_lt_self_iff {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), preorder (π i)] {x : Π (i : ι), π i} {i : ι} {a : π i} :
a < x a < x i
@[protected, instance]
def pi.has_sdiff {ι : Type u} {α : ι Type v} [Π (i : ι), has_sdiff (α i)] :
has_sdiff (Π (i : ι), α i)
Equations
theorem pi.sdiff_def {ι : Type u} {α : ι Type v} [Π (i : ι), has_sdiff (α i)] (x y : Π (i : ι), α i) :
x \ y = λ (i : ι), x i \ y i
@[simp]
theorem pi.sdiff_apply {ι : Type u} {α : ι Type v} [Π (i : ι), has_sdiff (α i)] (x y : Π (i : ι), α i) (i : ι) :
(x \ y) i = x i \ y i
@[simp]
theorem function.const_le_const {α : Type u} {β : Type v} [preorder α] [nonempty β] {a b : α} :
a b
@[simp]
theorem function.const_lt_const {α : Type u} {β : Type v} [preorder α] [nonempty β] {a b : α} :
< a < b

`min`/`max` recursors #

theorem min_rec {α : Type u} [linear_order α] {p : α Prop} {x y : α} (hx : x y p x) (hy : y x p y) :
p y)
theorem max_rec {α : Type u} [linear_order α] {p : α Prop} {x y : α} (hx : y x p x) (hy : x y p y) :
p y)
theorem min_rec' {α : Type u} [linear_order α] {x y : α} (p : α Prop) (hx : p x) (hy : p y) :
p y)
theorem max_rec' {α : Type u} [linear_order α] {x y : α} (p : α Prop) (hx : p x) (hy : p y) :
p y)
theorem min_def_lt {α : Type u} [linear_order α] (x y : α) :
= ite (x < y) x y
theorem max_def_lt {α : Type u} [linear_order α] (x y : α) :
= ite (x < y) y x

`has_sup` and `has_inf`#

@[class]
structure has_sup (α : Type u) :

Typeclass for the `⊔` (`\lub`) notation

Instances of this typeclass
Instances of other typeclasses for `has_sup`
• has_sup.has_sizeof_inst
@[class]
structure has_inf (α : Type u) :

Typeclass for the `⊓` (`\glb`) notation

Instances of this typeclass
Instances of other typeclasses for `has_inf`
• has_inf.has_sizeof_inst

Lifts of order instances #

@[reducible]
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
@[reducible]
def partial_order.lift {α : Type u_1} {β : Type u_2} (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
@[reducible]
def linear_order.lift {α : Type u_1} {β : Type u_2} [linear_order β] [has_sup α] [has_inf α] (f : α β) (inj : function.injective f) (hsup : (x y : α), f (x y) = linear_order.max (f x) (f y)) (hinf : (x y : α), f (x y) = linear_order.min (f x) (f y)) :

Transfer a `linear_order` on `β` to a `linear_order` on `α` using an injective function `f : α → β`. This version takes `[has_sup α]` and `[has_inf α]` as arguments, then uses them for `max` and `min` fields. See `linear_order.lift'` for a version that autogenerates `min` and `max` fields. See note [reducible non-instances].

Equations
@[reducible]
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 : α → β`. This version autogenerates `min` and `max` fields. See `linear_order.lift` for a version that takes `[has_sup α]` and `[has_inf α]`, then uses them as `max` and `min`. See note [reducible non-instances].

Equations
• inj = inj _ _

Subtype of an order #

@[protected, instance]
def subtype.has_le {α : Type u} [has_le α] {p : α Prop} :
Equations
@[protected, instance]
def subtype.has_lt {α : Type u} [has_lt α] {p : α Prop} :
Equations
@[simp]
theorem subtype.mk_le_mk {α : Type u} [has_le α] {p : α Prop} {x y : α} {hx : p x} {hy : p y} :
x, hx⟩ y, hy⟩ x y
@[simp]
theorem subtype.mk_lt_mk {α : Type u} [has_lt α] {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} [has_le α] {p : α Prop} {x y : subtype p} :
x y x y
@[simp, norm_cast]
theorem subtype.coe_lt_coe {α : Type u} [has_lt α] {p : α Prop} {x y : subtype p} :
x < y x < y
@[protected, instance]
def subtype.preorder {α : Type u} [preorder α] (p : α Prop) :
Equations
@[protected, instance]
def subtype.partial_order {α : Type u} (p : α Prop) :
Equations
@[protected, instance]
def subtype.decidable_le {α : Type u} [preorder α] {p : α Prop} :
Equations
@[protected, instance]
def subtype.decidable_lt {α : Type u} [preorder α] {p : α Prop} :
Equations
@[protected, instance]
def subtype.linear_order {α : Type u} [linear_order α] (p : α Prop) :

A subtype of a linear order is a linear order. We explicitly give the proofs of decidable equality and decidable order in order to ensure the decidability instances are all definitionally equal.

Equations

Pointwise order on `α × β`#

The lexicographic order is defined in `data.prod.lex`, 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₂
@[simp]
theorem prod.swap_le_swap {α : Type u} {β : Type v} [has_le α] [has_le β] {x y : α × β} :
x.swap y.swap x y
@[protected, instance]
def prod.preorder (α : Type u) (β : Type v) [preorder α] [preorder β] :
preorder × β)
Equations
@[simp]
theorem prod.swap_lt_swap {α : Type u} {β : Type v} [preorder α] [preorder β] {x y : α × β} :
x.swap < y.swap x < y
theorem prod.mk_le_mk_iff_left {α : Type u} {β : Type v} [preorder α] [preorder β] {a₁ a₂ : α} {b : β} :
(a₁, b) (a₂, b) a₁ a₂
theorem prod.mk_le_mk_iff_right {α : Type u} {β : Type v} [preorder α] [preorder β] {a : α} {b₁ b₂ : β} :
(a, b₁) (a, b₂) b₁ b₂
theorem prod.mk_lt_mk_iff_left {α : Type u} {β : Type v} [preorder α] [preorder β] {a₁ a₂ : α} {b : β} :
(a₁, b) < (a₂, b) a₁ < a₂
theorem prod.mk_lt_mk_iff_right {α : Type u} {β : Type v} [preorder α] [preorder β] {a : α} {b₁ b₂ : β} :
(a, b₁) < (a, b₂) b₁ < b₂
theorem prod.lt_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {x y : α × β} :
x < y x.fst < y.fst x.snd y.snd x.fst y.fst x.snd < y.snd
@[simp]
theorem prod.mk_lt_mk {α : Type u} {β : Type v} [preorder α] [preorder β] {a₁ a₂ : α} {b₁ b₂ : β} :
(a₁, b₁) < (a₂, b₂) a₁ < a₂ b₁ b₂ a₁ a₂ b₁ < b₂
@[protected, instance]
def prod.partial_order (α : Type u) (β : Type v)  :

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

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

Instances of this typeclass
theorem exists_between {α : Type u} [has_lt α] {a₁ a₂ : α} :
a₁ < a₂ ( (a : α), a₁ < a a < a₂)
@[protected, instance]
def order_dual.densely_ordered (α : Type u) [has_lt α]  :
@[simp]
theorem densely_ordered_order_dual {α : Type u} [has_lt α] :
@[protected, instance]
def prod.densely_ordered {α : Type u} {β : Type v} [preorder α] [preorder β]  :
@[protected, instance]
def pi.densely_ordered {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] [ (i : ι), densely_ordered (α i)] :
densely_ordered (Π (i : ι), α i)
theorem le_of_forall_le_of_dense {α : Type u} [linear_order α] {a₁ a₂ : α} (h : (a : α), a₂ < a a₁ a) :
a₁ a₂
theorem eq_of_le_of_forall_le_of_dense {α : Type u} [linear_order α] {a₁ a₂ : α} (h₁ : a₂ a₁) (h₂ : (a : α), a₂ < a a₁ a) :
a₁ = a₂
theorem le_of_forall_ge_of_dense {α : Type u} [linear_order α] {a₁ a₂ : α} (h : (a₃ : α), a₃ < a₁ a₃ a₂) :
a₁ a₂
theorem eq_of_le_of_forall_ge_of_dense {α : Type u} [linear_order α] {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₁
theorem eq_or_eq_or_eq_of_forall_not_lt_lt {α : Type u_1} [linear_order α] (h : ⦃x y z : α⦄, x < y y < z false) (x y z : α) :
x = y y = z x = z

If a linear order has no elements `x < y < z`, then it has at most two elements.

@[protected, instance]
Equations
theorem punit.max_eq (a b : punit) :
= punit.star
theorem punit.min_eq (a b : punit) :
= punit.star
@[protected, simp]
theorem punit.le (a b : punit) :
a b
@[simp]
theorem punit.not_lt (a b : punit) :
¬a < b
@[protected, instance]
@[protected, instance]
def Prop.has_le  :
has_le Prop

Propositions form a complete boolean algebra, where the `≤` relation is given by implication.

Equations
@[simp]
theorem le_Prop_eq  :
has_le.le = λ (_x _y : Prop), _x _y
theorem subrelation_iff_le {α : Type u} {r s : α α Prop} :
s r s
@[protected, instance]
Equations

Linear order from a total partial order #

def as_linear_order (α : Type u) :

Type synonym to create an instance of `linear_order` from a `partial_order` and `is_total α (≤)`

Equations
Instances for `as_linear_order`
@[protected, instance]
def as_linear_order.inhabited {α : Type u_1} [inhabited α] :
Equations
@[protected, instance]
noncomputable def as_linear_order.linear_order {α : Type u_1}  :
Equations