mathlib documentation

order.basic

Basic definitions about `≤` and `<` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. https://github.com/leanprover-community/mathlib4/pull/556 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} [partial_order α] {a b : α} :

a ≤ b → b ≤ a → b = a

theorem lt_of_le_of_ne' {α : Type u} [partial_order α] {a b : α} :

a ≤ b → b ≠ a → a < b

theorem ne.lt_of_le {α : Type u} [partial_order α] {a b : α} :

a ≠ b → a ≤ b → a < b

theorem ne.lt_of_le' {α : Type u} [partial_order α] {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 ↔ has_le.le = has_le.le

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} [partial_order α] {a b : α} :

a ≤ b → b ≤ a → a = b

Alias of le_antisymm.

theorem has_le.le.antisymm' {α : Type u} [partial_order α] {a b : α} :

a ≤ b → b ≤ a → b = a

Alias of ge_antisymm.

theorem has_le.le.lt_of_ne {α : Type u} [partial_order α] {a b : α} :

a ≤ b → a ≠ b → a < b

Alias of lt_of_le_of_ne.

theorem has_le.le.lt_of_ne' {α : Type u} [partial_order α] {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} [partial_order α] {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} [partial_order α] [decidable_rel has_le.le] {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} [partial_order α] {a b : α} (h : a ≤ b) :

a < b ↔ a ≠ b

theorem has_le.le.gt_iff_ne {α : Type u} [partial_order α] {a b : α} (h : a ≤ b) :

a < b ↔ b ≠ a

theorem has_le.le.not_lt_iff_eq {α : Type u} [partial_order α] {a b : α} (h : a ≤ b) :

¬a < b ↔ a = b

theorem has_le.le.not_gt_iff_eq {α : Type u} [partial_order α] {a b : α} (h : a ≤ b) :

¬a < b ↔ b = a

theorem has_le.le.le_iff_eq {α : Type u} [partial_order α] {a b : α} (h : a ≤ b) :

b ≤ a ↔ b = a

theorem has_le.le.ge_iff_eq {α : Type u} [partial_order α] {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) :

theorem has_lt.lt.not_le {α : Type u} [preorder α] {a b : α} (h : a < b) :

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} [partial_order α] [decidable_rel has_le.le] {a b : α} :

a ≤ b ↔ a = b ∨ a < b

theorem le_iff_eq_or_lt {α : Type u} [partial_order α] {a b : α} :

a ≤ b ↔ a = b ∨ a < b

theorem lt_iff_le_and_ne {α : Type u} [partial_order α] {a b : α} :

a < b ↔ a ≤ b ∧ a ≠ b

@[protected]

theorem decidable.eq_iff_le_not_lt {α : Type u} [partial_order α] [decidable_rel has_le.le] {a b : α} :

a = b ↔ a ≤ b ∧ ¬a < b

theorem eq_iff_le_not_lt {α : Type u} [partial_order α] {a b : α} :

a = b ↔ a ≤ b ∧ ¬a < b

theorem eq_or_lt_of_le {α : Type u} [partial_order α] {a b : α} (h : a ≤ b) :

a = b ∨ a < b

theorem eq_or_gt_of_le {α : Type u} [partial_order α] {a b : α} (h : a ≤ b) :

b = a ∨ a < b

@[nolint]

theorem has_le.le.eq_or_lt_dec {α : Type u} [partial_order α] [decidable_rel has_le.le] {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} [partial_order α] {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} [partial_order α] {a b : α} (h : a ≤ b) :

b = a ∨ a < b

Alias of eq_or_gt_of_le.

theorem eq_of_le_of_not_lt {α : Type u} [partial_order α] {a b : α} (hab : a ≤ b) (hba : ¬a < b) :

a = b

theorem eq_of_ge_of_not_gt {α : Type u} [partial_order α] {a b : α} (hab : a ≤ b) (hba : ¬a < b) :

b = a

theorem has_le.le.eq_of_not_lt {α : Type u} [partial_order α] {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} [partial_order α] {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} [partial_order α] {a b : α} (h : a ≠ b) :

a ≤ b ↔ a < b

theorem ne.not_le_or_not_le {α : Type u} [partial_order α] {a b : α} (h : a ≠ b) :

¬a ≤ b ∨ ¬b ≤ a

@[protected]

theorem decidable.ne_iff_lt_iff_le {α : Type u} [partial_order α] [decidable_eq α] {a b : α} :

a ≠ b ↔ a < b ↔ a ≤ b

@[simp]

theorem ne_iff_lt_iff_le {α : Type u} [partial_order α] {a b : α} :

a ≠ b ↔ a < b ↔ a ≤ b

theorem min_def' {α : Type u} [linear_order α] (a b : α) :

linear_order.min a b = ite (b ≤ a) b a

theorem max_def' {α : Type u} [linear_order α] (a b : α) :

linear_order.max 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} [partial_order α] {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} [partial_order α] {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} [partial_order β] (r : α → α → Prop) [is_symm α 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 →

@[ext]

theorem preorder.to_has_le_injective {α : Type u_1} :

function.injective (preorder.to_has_le α)

@[ext]

theorem partial_order.to_preorder_injective {α : Type u_1} :

function.injective (partial_order.to_preorder α)

@[ext]

theorem linear_order.to_partial_order_injective {α : Type u_1} :

function.injective (linear_order.to_partial_order α)

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

(f ⁻¹'o s) x y = s (f x) (f y)

Instances for order.preimage

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

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 α] :

nonempty αᵒᵈ

@[protected, instance]

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

subsingleton αᵒᵈ

@[protected, instance]

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

has_le αᵒᵈ

Equations

order_dual.has_le α = {le := λ (x y : α), y ≤ x}

@[protected, instance]

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

has_lt αᵒᵈ

Equations

order_dual.has_lt α = {lt := λ (x y : α), y < x}

@[protected, instance]

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

preorder αᵒᵈ

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

@[protected, instance]

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

partial_order αᵒᵈ

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

@[protected, instance]

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

linear_order αᵒᵈ

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 := infer_instance (λ (a b : α), has_le.le.decidable b a), decidable_eq := decidable_eq_of_decidable_le infer_instance, decidable_lt := infer_instance (λ (a b : α), has_lt.lt.decidable b a), max := linear_order.min _inst_1, max_def := _, min := linear_order.max _inst_1, min_def := _}

@[protected, instance]

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

inhabited αᵒᵈ

Equations

order_dual.inhabited = id

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

order_dual.preorder αᵒᵈ = H

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

order_dual.partial_order αᵒᵈ = H

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

order_dual.linear_order αᵒᵈ = H

`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

Prop.has_compl = {compl := not}

@[protected, instance]

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

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

Equations

pi.has_compl = {compl := λ (x : Π (i : ι), α i) (i : ι), (x i)ᶜ}

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) [is_irrefl α r] :

is_refl α rᶜ

@[protected, instance]

def is_refl.compl {α : Type u} (r : α → α → Prop) [is_refl α r] :

is_irrefl α 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

pi.has_le = {le := λ (x y : Π (i : ι), α i), ∀ (i : ι), x i ≤ y i}

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

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

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

pi.partial_order = {le := preorder.le pi.preorder, lt := preorder.lt pi.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

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

strong_lt a 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 : strong_lt a b) :

a ≤ b

theorem lt_of_strong_lt {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), preorder (π i)] {a b : Π (i : ι), π i} [nonempty ι] (h : strong_lt a 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 : strong_lt a b) (hbc : b ≤ 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 : strong_lt b c) :

theorem strong_lt.le {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), preorder (π i)] {a b : Π (i : ι), π i} (h : strong_lt a 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 : strong_lt a 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 : strong_lt a b) (hbc : b ≤ 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 : strong_lt b 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 ≤ function.update y i 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} :

function.update x 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} :

function.update x i a ≤ function.update y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j

@[simp]

theorem le_update_self_iff {ι : Type u_1} {π : ι → Type u_2} [decidable_eq ι] [Π (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} [decidable_eq ι] [Π (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} [decidable_eq ι] [Π (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} [decidable_eq ι] [Π (i : ι), preorder (π i)] {x : Π (i : ι), π i} {i : ι} {a : π i} :

function.update x 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

pi.has_sdiff = {sdiff := λ (x y : Π (i : ι), α i) (i : ι), x i \ y i}

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 : α} :

function.const β a ≤ function.const β b ↔ a ≤ b

@[simp]

theorem function.const_lt_const {α : Type u} {β : Type v} [preorder α] [nonempty β] {a b : α} :

function.const β a < function.const β 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 (linear_order.min x y)

theorem max_rec {α : Type u} [linear_order α] {p : α → Prop} {x y : α} (hx : y ≤ x → p x) (hy : x ≤ y → p y) :

p (linear_order.max x y)

theorem min_rec' {α : Type u} [linear_order α] {x y : α} (p : α → Prop) (hx : p x) (hy : p y) :

p (linear_order.min x y)

theorem max_rec' {α : Type u} [linear_order α] {x y : α} (p : α → Prop) (hx : p x) (hy : p y) :

p (linear_order.max x y)

theorem min_def_lt {α : Type u} [linear_order α] (x y : α) :

linear_order.min x y = ite (x < y) x y

theorem max_def_lt {α : Type u} [linear_order α] (x y : α) :

linear_order.max x y = ite (x < y) y x

`has_sup` and `has_inf` #

@[class]

structure has_sup (α : Type u) :

sup : α → α → α

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

inf : α → α → α

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

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

@[reducible]

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

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

linear_order α

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

linear_order.lift f inj hsup hinf = {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, max := has_sup.sup _inst_2, max_def := _, min := has_inf.inf _inst_3, min_def := _}

@[reducible]

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

linear_order.lift' f inj = linear_order.lift f inj _ _

Subtype of an order #

@[protected, instance]

def subtype.has_le {α : Type u} [has_le α] {p : α → Prop} :

has_le (subtype p)

Equations

subtype.has_le = {le := λ (x y : subtype p), ↑x ≤ ↑y}

@[protected, instance]

def subtype.has_lt {α : Type u} [has_lt α] {p : α → Prop} :

has_lt (subtype p)

Equations

subtype.has_lt = {lt := λ (x y : subtype p), ↑x < ↑y}

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

preorder (subtype p)

Equations

subtype.preorder p = preorder.lift coe

@[protected, instance]

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

partial_order (subtype p)

Equations

subtype.partial_order p = partial_order.lift coe subtype.coe_injective

@[protected, instance]

def subtype.decidable_le {α : Type u} [preorder α] [h : decidable_rel has_le.le] {p : α → Prop} :

decidable_rel has_le.le

Equations

subtype.decidable_le = λ (a b : subtype p), h ↑a ↑b

@[protected, instance]

def subtype.decidable_lt {α : Type u} [preorder α] [h : decidable_rel has_lt.lt] {p : α → Prop} :

decidable_rel has_lt.lt

Equations

subtype.decidable_lt = λ (a b : subtype p), h ↑a ↑b

@[protected, instance]

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

linear_order (subtype p)

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

subtype.linear_order p = linear_order.lift coe subtype.coe_injective _ _

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

prod.has_le α β = {le := λ (p q : α × β), p.fst ≤ q.fst ∧ p.snd ≤ q.snd}

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

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

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

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]

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 α] [densely_ordered α] {a₁ a₂ : α} :

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

@[protected, instance]

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

densely_ordered αᵒᵈ

@[simp]

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

densely_ordered αᵒᵈ ↔ densely_ordered α

@[protected, instance]

def prod.densely_ordered {α : Type u} {β : Type v} [preorder α] [preorder β] [densely_ordered α] [densely_ordered β] :

densely_ordered (α × β)

@[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 α] [densely_ordered α] {a₁ a₂ : α} (h : ∀ (a : α), a₂ < a → a₁ ≤ a) :

a₁ ≤ a₂

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

a₁ = a₂

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

a₁ ≤ a₂

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

a₁ = a₂

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

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

@[protected, instance]

def punit.linear_order :

linear_order punit

Equations

punit.linear_order = {le := λ (_x _x : punit), true, lt := λ (_x _x : punit), false, le_refl := punit.linear_order._proof_1, le_trans := punit.linear_order._proof_2, lt_iff_le_not_le := punit.linear_order._proof_3, le_antisymm := punit.linear_order._proof_4, le_total := punit.linear_order._proof_5, decidable_le := λ (_x _x : punit), decidable.true, decidable_eq := punit.decidable_eq, decidable_lt := λ (_x _x : punit), decidable.false, max := λ (_x _x : punit), punit.star, max_def := punit.linear_order._proof_6, min := λ (_x _x : punit), punit.star, min_def := punit.linear_order._proof_7}

theorem punit.max_eq (a b : punit) :

linear_order.max a b = punit.star

theorem punit.min_eq (a b : punit) :

linear_order.min a b = punit.star

@[protected, simp]

theorem punit.le (a b : punit) :

a ≤ b

@[simp]

theorem punit.not_lt (a b : punit) :

¬a < b

@[protected, instance]

def punit.densely_ordered :

densely_ordered punit

@[protected, instance]

def Prop.has_le :

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

Equations

Prop.has_le = {le := λ (_x _y : Prop), _x → _y}

@[simp]

theorem le_Prop_eq :

has_le.le = λ (_x _y : Prop), _x → _y

theorem subrelation_iff_le {α : Type u} {r s : α → α → Prop} :

subrelation r s ↔ r ≤ s

@[protected, instance]

def Prop.partial_order :

partial_order Prop

Equations

Prop.partial_order = {le := has_le.le Prop.has_le, lt := preorder.lt._default has_le.le, le_refl := Prop.partial_order._proof_1, le_trans := Prop.partial_order._proof_2, lt_iff_le_not_le := Prop.partial_order._proof_3, le_antisymm := Prop.partial_order._proof_4}

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

as_linear_order α = α

Instances for as_linear_order

@[protected, instance]

def as_linear_order.inhabited {α : Type u_1} [inhabited α] :

inhabited (as_linear_order α)

Equations

as_linear_order.inhabited = {default := inhabited.default _inst_1}

@[protected, instance]

noncomputable def as_linear_order.linear_order {α : Type u_1} [partial_order α] [is_total α has_le.le] :

linear_order (as_linear_order α)

Equations

as_linear_order.linear_order = {le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, 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), max := max_default (λ (a b : as_linear_order α), classical.dec_rel has_le.le a b), max_def := _, min := min_default (λ (a b : as_linear_order α), classical.dec_rel has_le.le a b), min_def := _}