Documentation

Mathlib.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 #

Transfering orders #

Extra class #

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 (LE.le) and < (LT.lt). To that end, we provide many aliases to dot notation-less lemmas. For example, le_trans is aliased with 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 LE.le.trans_lt and can be used to construct hab.trans hbc : a < c when hab : a ≤ b, hbc : b < c.

TODO #

Tags #

preorder, order, partial order, poset, linear order, chain

theorem le_trans' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b ca ba c
theorem lt_trans' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b < ca < ba < c
theorem lt_of_le_of_lt' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b ca < ba < c
theorem lt_of_lt_of_le' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b < ca ba < c
theorem ge_antisymm {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a bb ab = a
theorem lt_of_le_of_ne' {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a bb aa < b
theorem Ne.lt_of_le {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a ba ba < b
theorem Ne.lt_of_le' {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
b aa ba < b
theorem LE.ext {α : Type u} (x : LE α) (y : LE α) (le : LE.le = LE.le) :
x = y
theorem LE.ext_iff {α : Type u} (x : LE α) (y : LE α) :
x = y LE.le = LE.le
theorem LE.le.trans {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
a bb ca c

Alias of le_trans.

theorem LE.le.trans' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b ca ba c

Alias of le_trans'.

theorem LE.le.trans_lt {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
a bb < ca < c

Alias of lt_of_le_of_lt.

theorem LE.le.trans_lt' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b ca < ba < c

Alias of lt_of_le_of_lt'.

theorem LE.le.antisymm {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a bb aa = b

Alias of le_antisymm.

theorem LE.le.antisymm' {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a bb ab = a

Alias of ge_antisymm.

theorem LE.le.lt_of_ne {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a ba ba < b

Alias of lt_of_le_of_ne.

theorem LE.le.lt_of_ne' {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a bb aa < b

Alias of lt_of_le_of_ne'.

theorem LE.le.lt_of_not_le {α : Type u} [inst : Preorder α] {a : α} {b : α} :
a b¬b aa < b

Alias of lt_of_le_not_le.

theorem LE.le.lt_or_eq {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a ba < b a = b

Alias of lt_or_eq_of_le.

theorem LE.le.lt_or_eq_dec {α : Type u} [inst : PartialOrder α] [inst : DecidableRel fun x x_1 => x x_1] {a : α} {b : α} (hab : a b) :
a < b a = b

Alias of Decidable.lt_or_eq_of_le.

theorem LT.lt.le {α : Type u} [inst : Preorder α] {a : α} {b : α} :
a < ba b

Alias of le_of_lt.

theorem LT.lt.trans {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
a < bb < ca < c

Alias of lt_trans.

theorem LT.lt.trans' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b < ca < ba < c

Alias of lt_trans'.

theorem LT.lt.trans_le {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
a < bb ca < c

Alias of lt_of_lt_of_le.

theorem LT.lt.trans_le' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b < ca ba < c

Alias of lt_of_lt_of_le'.

theorem LT.lt.ne {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :
a b

Alias of ne_of_lt.

theorem LT.lt.asymm {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :
¬b < a

Alias of lt_asymm.

theorem LT.lt.not_lt {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :
¬b < a

Alias of lt_asymm.

theorem Eq.le {α : Type u} [inst : Preorder α] {a : α} {b : α} :
a = ba b

Alias of le_of_eq.

theorem le_rfl {α : Type u} [inst : Preorder α] {a : α} :
a a

A version of le_refl where the argument is implicit

@[simp]
theorem lt_self_iff_false {α : Type u} [inst : Preorder α] (x : α) :
x < x False
theorem le_of_le_of_eq {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} (hab : a b) (hbc : b = c) :
a c
theorem le_of_eq_of_le {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} (hab : a = b) (hbc : b c) :
a c
theorem lt_of_lt_of_eq {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} (hab : a < b) (hbc : b = c) :
a < c
theorem lt_of_eq_of_lt {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} (hab : a = b) (hbc : b < c) :
a < c
theorem le_of_le_of_eq' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b ca = ba c
theorem le_of_eq_of_le' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b = ca ba c
theorem lt_of_lt_of_eq' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b < ca = ba < c
theorem lt_of_eq_of_lt' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b = ca < ba < c
theorem LE.le.trans_eq {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} (hab : a b) (hbc : b = c) :
a c

Alias of le_of_le_of_eq.

theorem LE.le.trans_eq' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b ca = ba c

Alias of le_of_le_of_eq'.

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

Alias of lt_of_lt_of_eq.

theorem LT.lt.trans_eq' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :
b < ca = ba < c

Alias of lt_of_lt_of_eq'.

theorem Eq.trans_le {α : Type u} [inst : 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} [inst : Preorder α] {a : α} {b : α} {c : α} :
b = ca ba c

Alias of le_of_eq_of_le'.

theorem Eq.trans_lt {α : Type u} [inst : 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} [inst : Preorder α] {a : α} {b : α} {c : α} :
b = ca < ba < c

Alias of lt_of_eq_of_lt'.

theorem Eq.ge {α : Type u} [inst : 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} [inst : Preorder α] {x : α} {y : α} (h : x = y) :
¬x < y
theorem Eq.not_gt {α : Type u} [inst : Preorder α] {x : α} {y : α} (h : x = y) :
¬y < x
theorem LE.le.ge {α : Type u} [inst : LE α] {x : α} {y : α} (h : x y) :
y x
theorem LE.le.lt_iff_ne {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
a < b a b
theorem LE.le.gt_iff_ne {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
a < b b a
theorem LE.le.not_lt_iff_eq {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
¬a < b a = b
theorem LE.le.not_gt_iff_eq {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
¬a < b b = a
theorem LE.le.le_iff_eq {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
b a b = a
theorem LE.le.ge_iff_eq {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
b a a = b
theorem LE.le.lt_or_le {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : a b) (c : α) :
a < c c b
theorem LE.le.le_or_lt {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : a b) (c : α) :
a c c < b
theorem LE.le.le_or_le {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : a b) (c : α) :
a c c b
theorem LT.lt.gt {α : Type u} [inst : LT α] {x : α} {y : α} (h : x < y) :
y > x
theorem LT.lt.false {α : Type u} [inst : Preorder α] {x : α} :
x < xFalse
theorem LT.lt.ne' {α : Type u} [inst : Preorder α] {x : α} {y : α} (h : x < y) :
y x
theorem LT.lt.lt_or_lt {α : Type u} [inst : LinearOrder α] {x : α} {y : α} (h : x < y) (z : α) :
x < z z < y
theorem GE.ge.le {α : Type u} [inst : LE α] {x : α} {y : α} (h : x y) :
y x
theorem GT.gt.lt {α : Type u} [inst : LT α] {x : α} {y : α} (h : x > y) :
y < x
theorem ge_of_eq {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a = b) :
a b
@[simp]
theorem ge_iff_le {α : Type u} [inst : LE α] {a : α} {b : α} :
a b b a
@[simp]
theorem gt_iff_lt {α : Type u} [inst : LT α] {a : α} {b : α} :
a > b b < a
theorem not_le_of_lt {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :
¬b a
theorem LT.lt.not_le {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a < b) :
¬b a

Alias of not_le_of_lt.

theorem not_lt_of_le {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a b) :
¬b < a
theorem LE.le.not_lt {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a b) :
¬b < a

Alias of not_lt_of_le.

theorem ne_of_not_le {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : ¬a b) :
a b
theorem Decidable.le_iff_eq_or_lt {α : Type u} [inst : PartialOrder α] [inst : DecidableRel fun x x_1 => x x_1] {a : α} {b : α} :
a b a = b a < b
theorem le_iff_eq_or_lt {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a b a = b a < b
theorem lt_iff_le_and_ne {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a < b a b a b
theorem Decidable.eq_iff_le_not_lt {α : Type u} [inst : PartialOrder α] [inst : DecidableRel fun x x_1 => x x_1] {a : α} {b : α} :
a = b a b ¬a < b
theorem eq_iff_le_not_lt {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
a = b a b ¬a < b
theorem eq_or_lt_of_le {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
a = b a < b
theorem eq_or_gt_of_le {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
b = a a < b
theorem gt_or_eq_of_le {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
a < b b = a
theorem LE.le.eq_or_lt_dec {α : Type u} [inst : PartialOrder α] [inst : DecidableRel fun x x_1 => x x_1] {a : α} {b : α} (hab : a b) :
a = b a < b

Alias of Decidable.eq_or_lt_of_le.

theorem LE.le.eq_or_lt {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
a = b a < b

Alias of eq_or_lt_of_le.

theorem LE.le.eq_or_gt {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
b = a a < b

Alias of eq_or_gt_of_le.

theorem LE.le.gt_or_eq {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
a < b b = a

Alias of gt_or_eq_of_le.

theorem eq_of_le_of_not_lt {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (hab : a b) (hba : ¬a < b) :
a = b
theorem eq_of_ge_of_not_gt {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (hab : a b) (hba : ¬a < b) :
b = a
theorem LE.le.eq_of_not_lt {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (hab : a b) (hba : ¬a < b) :
a = b

Alias of eq_of_le_of_not_lt.

theorem LE.le.eq_of_not_gt {α : Type u} [inst : PartialOrder α] {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} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
a b a < b
theorem Ne.not_le_or_not_le {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (h : a b) :
¬a b ¬b a
theorem Decidable.ne_iff_lt_iff_le {α : Type u} [inst : PartialOrder α] [inst : DecidableEq α] {a : α} {b : α} :
(a b a < b) a b
@[simp]
theorem ne_iff_lt_iff_le {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :
(a b a < b) a b
theorem min_def' {α : Type u} [inst : LinearOrder α] (a : α) (b : α) :
min a b = if b a then b else a
theorem max_def' {α : Type u} [inst : LinearOrder α] (a : α) (b : α) :
max a b = if b a then a else b
theorem lt_of_not_le {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : ¬b a) :
a < b
theorem lt_iff_not_le {α : Type u} [inst : LinearOrder α] {x : α} {y : α} :
x < y ¬y x
theorem Ne.lt_or_lt {α : Type u} [inst : LinearOrder α] {x : α} {y : α} (h : x y) :
x < y y < x
@[simp]
theorem lt_or_lt_iff_ne {α : Type u} [inst : LinearOrder α] {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} [inst : LinearOrder α] {a : α} {b : α} :
¬a < b a = b b < a
theorem exists_ge_of_linear {α : Type u} [inst : LinearOrder α] (a : α) (b : α) :
c, a c b c
theorem lt_imp_lt_of_le_imp_le {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst : Preorder β] {a : α} {b : α} {c : β} {d : β} (H : a bc d) (h : d < c) :
b < a
theorem le_imp_le_iff_lt_imp_lt {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst : LinearOrder β] {a : α} {b : α} {c : β} {d : β} :
a bc d d < cb < a
theorem lt_iff_lt_of_le_iff_le' {α : Type u} {β : Type u_1} [inst : Preorder α] [inst : 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} [inst : LinearOrder α] [inst : LinearOrder β] {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} [inst : LinearOrder α] [inst : LinearOrder β] {a : α} {b : α} {c : β} {d : β} :
(a b c d) (b < a d < c)
theorem eq_of_forall_le_iff {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (H : ∀ (c : α), c a c b) :
a = b
theorem le_of_forall_le {α : Type u} [inst : Preorder α] {a : α} {b : α} (H : ∀ (c : α), c ac b) :
a b
theorem le_of_forall_le' {α : Type u} [inst : Preorder α] {a : α} {b : α} (H : ∀ (c : α), a cb c) :
b a
theorem le_of_forall_lt {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (H : ∀ (c : α), c < ac < b) :
a b
theorem forall_lt_iff_le {α : Type u} [inst : LinearOrder α] {a : α} {b : α} :
(∀ ⦃c : α⦄, c < ac < b) a b
theorem le_of_forall_lt' {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (H : ∀ (c : α), a < cb < c) :
b a
theorem forall_lt_iff_le' {α : Type u} [inst : LinearOrder α] {a : α} {b : α} :
(∀ ⦃c : α⦄, a < cb < c) b a
theorem eq_of_forall_ge_iff {α : Type u} [inst : PartialOrder α] {a : α} {b : α} (H : ∀ (c : α), a c b c) :
a = b
theorem eq_of_forall_lt_iff {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : ∀ (c : α), c < a c < b) :
a = b
theorem eq_of_forall_gt_iff {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : ∀ (c : α), a < c b < c) :
a = b
theorem rel_imp_eq_of_rel_imp_le {α : Type u} {β : Type v} [inst : PartialOrder β] (r : ααProp) [inst : IsSymm α r] {f : αβ} (h : ∀ (a b : α), r a bf a f b) {a : α} {b : α} :
r a bf 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 : α} [inst : Preorder α] (hca : c a) (hbd : b d) :
a bc d

monotonicity of with respect to

theorem commutative_of_le {α : Type u} {β : Type v} [inst : PartialOrder α] {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} [inst : PartialOrder α] {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.

theorem Preorder.ext {α : Type u_1} {A : Preorder α} {B : Preorder α} (H : ∀ (x y : α), x y x y) :
A = B
theorem PartialOrder.ext {α : Type u_1} {A : PartialOrder α} {B : PartialOrder α} (H : ∀ (x y : α), x y x y) :
A = B
theorem LinearOrder.ext {α : Type u_1} {A : LinearOrder α} {B : LinearOrder α} (H : ∀ (x y : α), x y x y) :
A = B
def Order.Preimage {α : Sort u_1} {β : Sort u_2} (f : αβ) (s : ββProp) (x : α) (y : α) :

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 RelEmbedding (assuming f is injective).

Equations

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 RelEmbedding (assuming f is injective).

Equations
instance Order.Preimage.decidable {α : Sort u_1} {β : Sort u_2} (f : αβ) (s : ββProp) [H : DecidableRel s] :

The preimage of a decidable order is decidable.

Equations

Order dual #

def OrderDual (α : Type u_1) :
Type u_1

Type synonym to equip a type with the dual order: means and < means >. αᵒᵈ is notation for OrderDual α.

Equations

Type synonym to equip a type with the dual order: means and < means >. αᵒᵈ is notation for OrderDual α.

Equations
instance OrderDual.instLEOrderDual (α : Type u_1) [inst : LE α] :
Equations
instance OrderDual.instLTOrderDual (α : Type u_1) [inst : LT α] :
Equations
instance OrderDual.preorder (α : Type u_1) [inst : Preorder α] :
Equations
instance OrderDual.partialOrder (α : Type u_1) [inst : PartialOrder α] :
Equations
instance OrderDual.linearOrder (α : Type u_1) [inst : LinearOrder α] :
Equations
Equations
  • OrderDual.instForAllInhabitedOrderDual = x

HasCompl #

class HasCompl (α : Type u_1) :
Type u_1
  • Set / lattice complement

    compl : αα

Set / lattice complement

Instances
    Equations
    instance Pi.hasCompl {ι : Type u} {α : ιType v} [inst : (i : ι) → HasCompl (α i)] :
    HasCompl ((i : ι) → α i)
    Equations
    • Pi.hasCompl = { compl := fun x i => x i }
    theorem Pi.compl_def {ι : Type u} {α : ιType v} [inst : (i : ι) → HasCompl (α i)] (x : (i : ι) → α i) :
    x = fun i => x i
    @[simp]
    theorem Pi.compl_apply {ι : Type u} {α : ιType v} [inst : (i : ι) → HasCompl (α i)] (x : (i : ι) → α i) (i : ι) :
    (((i : ι) → α i)) Pi.hasCompl x i = x i
    instance IsIrrefl.compl {α : Type u} (r : ααProp) [inst : IsIrrefl α r] :
    IsRefl α (r)
    Equations
    instance IsRefl.compl {α : Type u} (r : ααProp) [inst : IsRefl α r] :
    Equations

    Order instances on the function space #

    instance Pi.hasLe {ι : Type u} {α : ιType v} [inst : (i : ι) → LE (α i)] :
    LE ((i : ι) → α i)
    Equations
    • Pi.hasLe = { le := fun x y => ∀ (i : ι), x i y i }
    theorem Pi.le_def {ι : Type u} {α : ιType v} [inst : (i : ι) → LE (α i)] {x : (i : ι) → α i} {y : (i : ι) → α i} :
    x y ∀ (i : ι), x i y i
    instance Pi.preorder {ι : Type u} {α : ιType v} [inst : (i : ι) → Preorder (α i)] :
    Preorder ((i : ι) → α i)
    Equations
    • Pi.preorder = let src := inferInstanceAs (LE ((i : ι) → α i)); Preorder.mk (_ : ∀ (a : (i : ι) → α i) (i : ι), a i a i) (_ : ∀ (a b c : (i : ι) → α i), a bb c∀ (i : ι), a i c i)
    theorem Pi.lt_def {ι : Type u} {α : ιType v} [inst : (i : ι) → Preorder (α i)] {x : (i : ι) → α i} {y : (i : ι) → α i} :
    x < y x y i, x i < y i
    instance Pi.partialOrder {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → PartialOrder (π i)] :
    PartialOrder ((i : ι) → π i)
    Equations
    • Pi.partialOrder = let src := Pi.preorder; PartialOrder.mk (_ : ∀ (x x_1 : (i : ι) → π i), x x_1x_1 xx = x_1)
    def StrongLT {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → LT (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) :

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

    Equations
    theorem le_of_strongLT {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} (h : StrongLT a b) :
    a b
    theorem lt_of_strongLT {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} [inst : Nonempty ι] (h : StrongLT a b) :
    a < b
    theorem strongLT_of_strongLT_of_le {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {c : (i : ι) → π i} (hab : StrongLT a b) (hbc : b c) :
    theorem strongLT_of_le_of_strongLT {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {c : (i : ι) → π i} (hab : a b) (hbc : StrongLT b c) :
    theorem StrongLT.le {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} (h : StrongLT a b) :
    a b

    Alias of le_of_strongLT.

    theorem StrongLT.lt {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} [inst : Nonempty ι] (h : StrongLT a b) :
    a < b

    Alias of lt_of_strongLT.

    theorem StrongLT.trans_le {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {c : (i : ι) → π i} (hab : StrongLT a b) (hbc : b c) :

    Alias of strongLT_of_strongLT_of_le.

    theorem LE.le.trans_strongLT {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {c : (i : ι) → π i} (hab : a b) (hbc : StrongLT b c) :

    Alias of strongLT_of_le_of_strongLT.

    theorem le_update_iff {ι : Type u_1} {π : ιType u_2} [inst : DecidableEq ι] [inst : (i : ι) → Preorder (π i)] {x : (i : ι) → π i} {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_1} {π : ιType u_2} [inst : DecidableEq ι] [inst : (i : ι) → Preorder (π i)] {x : (i : ι) → π i} {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_1} {π : ιType u_2} [inst : DecidableEq ι] [inst : (i : ι) → Preorder (π i)] {x : (i : ι) → π i} {y : (i : ι) → π i} {i : ι} {a : π i} {b : π i} :
    Function.update x i a Function.update y i b a b ∀ (j : ι), j ix j y j
    @[simp]
    theorem le_update_self_iff {ι : Type u_1} {π : ιType u_2} [inst : DecidableEq ι] [inst : (i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
    x Function.update x i a x i a
    @[simp]
    theorem update_le_self_iff {ι : Type u_1} {π : ιType u_2} [inst : DecidableEq ι] [inst : (i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
    Function.update x i a x a x i
    @[simp]
    theorem lt_update_self_iff {ι : Type u_1} {π : ιType u_2} [inst : DecidableEq ι] [inst : (i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
    x < Function.update x i a x i < a
    @[simp]
    theorem update_lt_self_iff {ι : Type u_1} {π : ιType u_2} [inst : DecidableEq ι] [inst : (i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
    Function.update x i a < x a < x i
    instance Pi.sdiff {ι : Type u} {α : ιType v} [inst : (i : ι) → SDiff (α i)] :
    SDiff ((i : ι) → α i)
    Equations
    • Pi.sdiff = { sdiff := fun x y i => x i \ y i }
    theorem Pi.sdiff_def {ι : Type u} {α : ιType v} [inst : (i : ι) → SDiff (α i)] (x : (i : ι) → α i) (y : (i : ι) → α i) :
    x \ y = fun i => x i \ y i
    @[simp]
    theorem Pi.sdiff_apply {ι : Type u} {α : ιType v} [inst : (i : ι) → SDiff (α i)] (x : (i : ι) → α i) (y : (i : ι) → α i) (i : ι) :
    (((i : ι) → α i) \ Pi.sdiff) x y i = x i \ y i
    @[simp]
    theorem Function.const_le_const {α : Type u} {β : Type v} [inst : Preorder α] [inst : Nonempty β] {a : α} {b : α} :
    @[simp]
    theorem Function.const_lt_const {α : Type u} {β : Type v} [inst : Preorder α] [inst : Nonempty β] {a : α} {b : α} :

    min/max recursors #

    theorem min_rec {α : Type u} [inst : LinearOrder α] {p : αProp} {x : α} {y : α} (hx : x yp x) (hy : y xp y) :
    p (min x y)
    theorem max_rec {α : Type u} [inst : LinearOrder α] {p : αProp} {x : α} {y : α} (hx : y xp x) (hy : x yp y) :
    p (max x y)
    theorem min_rec' {α : Type u} [inst : LinearOrder α] {x : α} {y : α} (p : αProp) (hx : p x) (hy : p y) :
    p (min x y)
    theorem max_rec' {α : Type u} [inst : LinearOrder α] {x : α} {y : α} (p : αProp) (hx : p x) (hy : p y) :
    p (max x y)
    theorem min_def_lt {α : Type u} [inst : LinearOrder α] (x : α) (y : α) :
    min x y = if x < y then x else y
    theorem max_def_lt {α : Type u} [inst : LinearOrder α] (x : α) (y : α) :
    max x y = if x < y then y else x

    Sup and Inf #

    theorem Sup.ext_iff {α : Type u} (x : Sup α) (y : Sup α) :
    x = y Sup.sup = Sup.sup
    theorem Sup.ext {α : Type u} (x : Sup α) (y : Sup α) (sup : Sup.sup = Sup.sup) :
    x = y
    class Sup (α : Type u) :
    • Least upper bound (\lub notation)

      sup : ααα

    Typeclass for the (\lub) notation

    Instances
      theorem Inf.ext {α : Type u} (x : Inf α) (y : Inf α) (inf : Inf.inf = Inf.inf) :
      x = y
      theorem Inf.ext_iff {α : Type u} (x : Inf α) (y : Inf α) :
      x = y Inf.inf = Inf.inf
      class Inf (α : Type u) :
      • Greatest lower bound (\glb notation)

        inf : ααα

      Typeclass for the (\glb) notation

      Instances

        Greatest lower bound (\glb notation)

        Equations

        Lifts of order instances #

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

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

        Equations
        def PartialOrder.lift {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] (f : αβ) (inj : Function.Injective f) :

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

        Equations
        theorem compare_of_injective_eq_compareOfLessAndEq {α : Type u} {β : Type v} (a : α) (b : α) [inst : LinearOrder β] [inst : DecidableEq α] (f : αβ) (inj : Function.Injective f) [inst : Decidable (a < b)] :
        compare (f a) (f b) = compareOfLessAndEq a b
        def LinearOrder.lift {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] [inst : Sup α] [inst : Inf α] (f : αβ) (inj : Function.Injective f) (hsup : ∀ (x y : α), f (x y) = max (f x) (f y)) (hinf : ∀ (x y : α), f (x y) = min (f x) (f y)) :

        Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version takes [Sup α] and [Inf α] as arguments, then uses them for max and min fields. See LinearOrder.lift' for a version that autogenerates min and max fields, and LinearOrder.liftWithOrd for one that does not auto-generate compare fields. See note [reducible non-instances].

        Equations
        • One or more equations did not get rendered due to their size.
        def LinearOrder.lift' {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] (f : αβ) (inj : Function.Injective f) :

        Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version autogenerates min and max fields. See LinearOrder.lift for a version that takes [Sup α] and [Inf α], then uses them as max and min. See LinearOrder.liftWithOrd' for a version which does not auto-generate compare fields. See note [reducible non-instances].

        Equations
        • One or more equations did not get rendered due to their size.
        def LinearOrder.liftWithOrd {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] [inst : Sup α] [inst : Inf α] [inst : Ord α] (f : αβ) (inj : Function.Injective f) (hsup : ∀ (x y : α), f (x y) = max (f x) (f y)) (hinf : ∀ (x y : α), f (x y) = min (f x) (f y)) (compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)) :

        Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version takes [Sup α] and [Inf α] as arguments, then uses them for max and min fields. It also takes [Ord α] as an argument and uses them for compare fields. See LinearOrder.lift for a version that autogenerates compare fields, and LinearOrder.liftWithOrd' for one that auto-generates min and max fields. fields. See note [reducible non-instances].

        Equations
        • One or more equations did not get rendered due to their size.
        def LinearOrder.liftWithOrd' {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] [inst : Ord α] (f : αβ) (inj : Function.Injective f) (compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)) :

        Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version auto-generates min and max fields. It also takes [Ord α] as an argument and uses them for compare fields. See LinearOrder.lift for a version that autogenerates compare fields, and LinearOrder.liftWithOrd for one that doesn't auto-generate min and max fields. fields. See note [reducible non-instances].

        Equations
        • One or more equations did not get rendered due to their size.

        Subtype of an order #

        instance Subtype.le {α : Type u} [inst : LE α] {p : αProp} :
        Equations
        • Subtype.le = { le := fun x y => x y }
        instance Subtype.lt {α : Type u} [inst : LT α] {p : αProp} :
        Equations
        • Subtype.lt = { lt := fun x y => x < y }
        @[simp]
        theorem Subtype.mk_le_mk {α : Type u} [inst : LE α] {p : αProp} {x : α} {y : α} {hx : p x} {hy : p y} :
        { val := x, property := hx } { val := y, property := hy } x y
        @[simp]
        theorem Subtype.mk_lt_mk {α : Type u} [inst : LT α] {p : αProp} {x : α} {y : α} {hx : p x} {hy : p y} :
        { val := x, property := hx } < { val := y, property := hy } x < y
        @[simp]
        theorem Subtype.coe_le_coe {α : Type u} [inst : LE α] {p : αProp} {x : Subtype p} {y : Subtype p} :
        x y x y
        @[simp]
        theorem Subtype.coe_lt_coe {α : Type u} [inst : LT α] {p : αProp} {x : Subtype p} {y : Subtype p} :
        x < y x < y
        instance Subtype.preorder {α : Type u} [inst : Preorder α] (p : αProp) :
        Equations
        instance Subtype.partialOrder {α : Type u} [inst : PartialOrder α] (p : αProp) :
        Equations
        instance Subtype.decidableLE {α : Type u} [inst : Preorder α] [h : DecidableRel fun x x_1 => x x_1] {p : αProp} :
        DecidableRel fun x x_1 => x x_1
        Equations
        instance Subtype.decidableLT {α : Type u} [inst : Preorder α] [h : DecidableRel fun x x_1 => x < x_1] {p : αProp} :
        DecidableRel fun x x_1 => x < x_1
        Equations
        instance Subtype.linearOrder {α : Type u} [inst : LinearOrder α] (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
        • One or more equations did not get rendered due to their size.

        Pointwise order on α × β #

        The lexicographic order is defined in Data.Prod.Lex, and the instances are available via the type synonym α ×ₗ β = α × β.

        instance Prod.instLEProd (α : Type u) (β : Type v) [inst : LE α] [inst : LE β] :
        LE (α × β)
        Equations
        theorem Prod.le_def {α : Type u} {β : Type v} [inst : LE α] [inst : LE β] {x : α × β} {y : α × β} :
        x y x.fst y.fst x.snd y.snd
        @[simp]
        theorem Prod.mk_le_mk {α : Type u} {β : Type v} [inst : LE α] [inst : LE β] {x₁ : α} {x₂ : α} {y₁ : β} {y₂ : β} :
        (x₁, y₁) (x₂, y₂) x₁ x₂ y₁ y₂
        @[simp]
        theorem Prod.swap_le_swap {α : Type u} {β : Type v} [inst : LE α] [inst : LE β] {x : α × β} {y : α × β} :
        instance Prod.instPreorderProd (α : Type u) (β : Type v) [inst : Preorder α] [inst : Preorder β] :
        Preorder (α × β)
        Equations
        @[simp]
        theorem Prod.swap_lt_swap {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {x : α × β} {y : α × β} :
        theorem Prod.mk_le_mk_iff_left {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {a₁ : α} {a₂ : α} {b : β} :
        (a₁, b) (a₂, b) a₁ a₂
        theorem Prod.mk_le_mk_iff_right {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {a : α} {b₁ : β} {b₂ : β} :
        (a, b₁) (a, b₂) b₁ b₂
        theorem Prod.mk_lt_mk_iff_left {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {a₁ : α} {a₂ : α} {b : β} :
        (a₁, b) < (a₂, b) a₁ < a₂
        theorem Prod.mk_lt_mk_iff_right {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {a : α} {b₁ : β} {b₂ : β} :
        (a, b₁) < (a, b₂) b₁ < b₂
        theorem Prod.lt_iff {α : Type u} {β : Type v} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : Preorder β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} :
        (a₁, b₁) < (a₂, b₂) a₁ < a₂ b₁ b₂ a₁ a₂ b₁ < b₂
        instance Prod.instPartialOrderProd (α : Type u) (β : Type v) [inst : PartialOrder α] [inst : PartialOrder β] :

        The pointwise partial order on a product. (The lexicographic ordering is defined in Order.Lexicographic, and the instances are available via the type synonym α ×ₗ β = α × β.)

        Equations

        Additional order classes #

        class DenselyOrdered (α : Type u) [inst : LT α] :
        • An order is dense if there is an element between any pair of distinct elements.

          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
          theorem exists_between {α : Type u} [inst : LT α] [inst : DenselyOrdered α] {a₁ : α} {a₂ : α} :
          a₁ < a₂a, a₁ < a a < a₂
          instance instDenselyOrderedForAllToLTPreorder {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → Preorder (α i)] [inst : ∀ (i : ι), DenselyOrdered (α i)] :
          DenselyOrdered ((i : ι) → α i)
          Equations
          theorem le_of_forall_le_of_dense {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] {a₁ : α} {a₂ : α} (h : ∀ (a : α), a₂ < aa₁ a) :
          a₁ a₂
          theorem eq_of_le_of_forall_le_of_dense {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] {a₁ : α} {a₂ : α} (h₁ : a₂ a₁) (h₂ : ∀ (a : α), a₂ < aa₁ a) :
          a₁ = a₂
          theorem le_of_forall_ge_of_dense {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] {a₁ : α} {a₂ : α} (h : ∀ (a₃ : α), a₃ < a₁a₃ a₂) :
          a₁ a₂
          theorem eq_of_le_of_forall_ge_of_dense {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] {a₁ : α} {a₂ : α} (h₁ : a₂ a₁) (h₂ : ∀ (a₃ : α), a₃ < a₁a₃ a₂) :
          a₁ = a₂
          theorem dense_or_discrete {α : Type u} [inst : LinearOrder α] (a₁ : α) (a₂ : α) :
          (a, a₁ < a a < a₂) (∀ (a : α), a₁ < aa₂ a) ∀ (a : α), a < a₂a a₁
          theorem eq_or_eq_or_eq_of_forall_not_lt_lt {α : Type u} [inst : LinearOrder α] (h : ∀ ⦃x y z : α⦄, x < yy < zFalse) (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.

          Equations
          • One or more equations did not get rendered due to their size.
          theorem PUnit.max_eq (a : PUnit) (b : PUnit) {star : PUnit} :
          max a b = star
          theorem PUnit.min_eq (a : PUnit) (b : PUnit) {star : PUnit} :
          min a b = star
          theorem PUnit.le (a : PUnit) (b : PUnit) :
          a b
          theorem PUnit.not_lt (a : PUnit) (b : PUnit) :
          ¬a < b
          instance Prop.le :

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

          Equations
          • Prop.le = { le := fun x x_1 => xx_1 }
          @[simp]
          theorem le_Prop_eq :
          (fun x x_1 => x x_1) = fun x x_1 => xx_1
          theorem subrelation_iff_le {α : Type u} {r : ααProp} {s : ααProp} :

          Linear order from a total partial order #

          def AsLinearOrder (α : Type u) :

          Type synonym to create an instance of LinearOrder from a PartialOrder and IsTotal α (≤)

          Equations
          instance instInhabitedAsLinearOrder {α : Type u_1} [inst : Inhabited α] :
          Equations
          • instInhabitedAsLinearOrder = { default := default }
          noncomputable instance AsLinearOrder.linearOrder {α : Type u_1} [inst : PartialOrder α] [inst : IsTotal α fun x x_1 => x x_1] :
          Equations
          • One or more equations did not get rendered due to their size.