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 #

OrderDual α : A type synonym reversing the meaning of all inequalities, with notation αᵒᵈ.
AsLinearOrder α: A type synonym to promote PartialOrder α to LinearOrder α using IsTotal α (≤).

Transfering orders #

Order.Preimage, Preorder.lift: Transfers a (pre)order on β to an order on α using a function f : α → β.
PartialOrder.lift, LinearOrder.lift: Transfers a partial (resp., linear) order on β to a partial (resp., linear) order on α using an injective function f.

Extra class #

Sup: type class for the ⊔ notation
Inf: type class for the ⊓ notation
HasCompl: type class for the ᶜ notation
DenselyOrdered: 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 ≤ (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 #

expand module docs
automatic construction of dual definitions / theorems

Tags #

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

theorem le_trans' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :

b ≤ c → a ≤ b → a ≤ c

theorem lt_trans' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :

b < c → a < b → a < c

theorem lt_of_le_of_lt' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :

b ≤ c → a < b → a < c

theorem lt_of_lt_of_le' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :

b < c → a ≤ b → a < c

theorem ge_antisymm {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :

a ≤ b → b ≤ a → b = a

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

a ≤ b → b ≠ a → a < b

theorem Ne.lt_of_le {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :

a ≠ b → a ≤ b → a < b

theorem Ne.lt_of_le' {α : Type u} [inst : PartialOrder α] {a : α} {b : α} :

b ≠ a → a ≤ b → a < 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 ≤ b → b ≤ c → a ≤ c

Alias of le_trans.

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

b ≤ c → a ≤ b → a ≤ c

Alias of le_trans'.

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

a ≤ b → b < c → a < c

Alias of lt_of_le_of_lt.

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

b ≤ c → a < b → a < c

Alias of lt_of_le_of_lt'.

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

a ≤ b → b ≤ a → a = b

Alias of le_antisymm.

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

a ≤ b → b ≤ a → b = a

Alias of ge_antisymm.

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

a ≤ b → a ≠ b → a < b

Alias of lt_of_le_of_ne.

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

a ≤ b → b ≠ a → a < b

Alias of lt_of_le_of_ne'.

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

a ≤ b → ¬b ≤ a → a < b

Alias of lt_of_le_not_le.

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

a ≤ b → a < 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 < b → a ≤ b

Alias of le_of_lt.

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

a < b → b < c → a < c

Alias of lt_trans.

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

b < c → a < b → a < c

Alias of lt_trans'.

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

a < b → b ≤ c → a < c

Alias of lt_of_lt_of_le.

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

b < c → a ≤ b → a < 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 = b → a ≤ 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 ≤ c → a = b → a ≤ c

theorem le_of_eq_of_le' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :

b = c → a ≤ b → a ≤ c

theorem lt_of_lt_of_eq' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :

b < c → a = b → a < c

theorem lt_of_eq_of_lt' {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} :

b = c → a < b → a < 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 ≤ c → a = b → a ≤ 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 < c → a = b → a < 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 = c → a ≤ b → a ≤ 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 = c → a < b → a < 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 < x → False

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

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

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 ≤ b → c ≤ 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 ≤ b → c ≤ d ↔ d < c → b < 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 ≤ a → c ≤ b) :

a ≤ b

theorem le_of_forall_le' {α : Type u} [inst : Preorder α] {a : α} {b : α} (H : ∀ (c : α), a ≤ c → b ≤ c) :

b ≤ a

theorem le_of_forall_lt {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (H : ∀ (c : α), c < a → c < b) :

a ≤ b

theorem forall_lt_iff_le {α : Type u} [inst : LinearOrder α] {a : α} {b : α} :

(∀ ⦃c : α⦄, c < a → c < b) ↔ a ≤ b

theorem le_of_forall_lt' {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (H : ∀ (c : α), a < c → b < c) :

b ≤ a

theorem forall_lt_iff_le' {α : Type u} [inst : LinearOrder α] {a : α} {b : α} :

(∀ ⦃c : α⦄, a < c → b < 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 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 : α} [inst : Preorder α] (hca : c ≤ a) (hbd : b ≤ d) :

a ≤ b → c ≤ 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.toLE_injective {α : Type u_1} :

Function.Injective (@Preorder.toLE α)

theorem PartialOrder.toPreorder_injective {α : Type u_1} :

Function.Injective (@PartialOrder.toPreorder α)

theorem LinearOrder.toPartialOrder_injective {α : Type u_1} :

Function.Injective (@LinearOrder.toPartialOrder α)

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

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

def «term_⁻¹'o_» :

Lean.TrailingParserDescr

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

«term_⁻¹'o_» = Lean.ParserDescr.trailingNode `term_⁻¹'o_ 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁻¹'o ") (Lean.ParserDescr.cat `term 81))

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

DecidableRel (f ⁻¹'o s)

The preimage of a decidable order is decidable.

Equations

Order.Preimage.decidable f s x x = H (f x) (f x)

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

αᵒᵈ = α

def «term_ᵒᵈ» :

Lean.TrailingParserDescr

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

Equations

«term_ᵒᵈ» = Lean.ParserDescr.trailingNode `term_ᵒᵈ 1024 0 (Lean.ParserDescr.symbol "ᵒᵈ")

instance OrderDual.instNonemptyOrderDual (α : Type u_1) [h : Nonempty α] :

Nonempty αᵒᵈ

Equations

OrderDual.instNonemptyOrderDual = OrderDual.instNonemptyOrderDual.proof_1

instance OrderDual.instSubsingletonOrderDual (α : Type u_1) [h : Subsingleton α] :

Subsingleton αᵒᵈ

Equations

OrderDual.instSubsingletonOrderDual = OrderDual.instSubsingletonOrderDual.proof_1

instance OrderDual.instLEOrderDual (α : Type u_1) [inst : LE α] :

Equations

OrderDual.instLEOrderDual α = { le := fun x y => y ≤ x }

instance OrderDual.instLTOrderDual (α : Type u_1) [inst : LT α] :

Equations

OrderDual.instLTOrderDual α = { lt := fun x y => y < x }

instance OrderDual.preorder (α : Type u_1) [inst : Preorder α] :

Preorder αᵒᵈ

Equations

OrderDual.preorder α = Preorder.mk (_ : ∀ (x : αᵒᵈ), x ≤ x) (_ : ∀ (x x_1 x_2 : αᵒᵈ), x ≤ x_1 → x_1 ≤ x_2 → x_2 ≤ x)

instance OrderDual.partialOrder (α : Type u_1) [inst : PartialOrder α] :

PartialOrder αᵒᵈ

Equations

OrderDual.partialOrder α = let src := inferInstanceAs (Preorder αᵒᵈ); PartialOrder.mk (_ : ∀ (a b : αᵒᵈ), a ≤ b → b ≤ a → a = b)

instance OrderDual.linearOrder (α : Type u_1) [inst : LinearOrder α] :

LinearOrder αᵒᵈ

Equations

OrderDual.linearOrder α = let src := inferInstanceAs (PartialOrder αᵒᵈ); LinearOrder.mk (_ : ∀ (a b : α), b ≤ a ∨ a ≤ b) inferInstance decidableEq_of_decidableLE inferInstance

instance OrderDual.instForAllInhabitedOrderDual {α : Type u} [inst : Inhabited α] :

Inhabited αᵒᵈ

Equations

OrderDual.instForAllInhabitedOrderDual = x

theorem OrderDual.Preorder.dual_dual (α : Type u_1) [H : Preorder α] :

OrderDual.preorder αᵒᵈ = H

theorem OrderDual.partialOrder.dual_dual (α : Type u_1) [H : PartialOrder α] :

OrderDual.partialOrder αᵒᵈ = H

theorem OrderDual.linearOrder.dual_dual (α : Type u_1) [H : LinearOrder α] :

OrderDual.linearOrder αᵒᵈ = H

`HasCompl` #

class HasCompl (α : Type u_1) :

Type u_1

Set / lattice complement
compl : α → α

Set / lattice complement

Instances

def «term_ᶜ» :

Lean.TrailingParserDescr

Set / lattice complement

Equations

«term_ᶜ» = Lean.ParserDescr.trailingNode `term_ᶜ 999 999 (Lean.ParserDescr.symbol "ᶜ")

instance Prop.hasCompl :

Equations

Prop.hasCompl = { compl := Not }

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

@IsIrrefl.compl = @IsIrrefl.compl.proof_1

instance IsRefl.compl {α : Type u} (r : α → α → Prop) [inst : IsRefl α r] :

IsIrrefl α (rᶜ)

Equations

@IsRefl.compl = @IsRefl.compl.proof_1

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 ≤ b → b ≤ 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_1 → x_1 ≤ x → x = 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

StrongLT a b = ∀ (i : ι), a i < b i

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 ≠ i → x 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 ≠ i → x 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 ≠ i → x 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 : α} :

Function.const β a ≤ Function.const β b ↔ a ≤ b

@[simp]

theorem Function.const_lt_const {α : Type u} {β : Type v} [inst : Preorder α] [inst : Nonempty β] {a : α} {b : α} :

Function.const β a < Function.const β b ↔ a < b

`min`/`max` recursors #

theorem min_rec {α : Type u} [inst : LinearOrder α] {p : α → Prop} {x : α} {y : α} (hx : x ≤ y → p x) (hy : y ≤ x → p y) :

p (min x y)

theorem max_rec {α : Type u} [inst : LinearOrder α] {p : α → Prop} {x : α} {y : α} (hx : y ≤ x → p x) (hy : x ≤ y → p 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

def «term_⊔_» :

Lean.TrailingParserDescr

Least upper bound (\lub notation)

Equations

«term_⊔_» = Lean.ParserDescr.trailingNode `term_⊔_ 68 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊔ ") (Lean.ParserDescr.cat `term 69))

def «term_⊓_» :

Lean.TrailingParserDescr

Greatest lower bound (\glb notation)

Equations

«term_⊓_» = Lean.ParserDescr.trailingNode `term_⊓_ 69 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓ ") (Lean.ParserDescr.cat `term 70))

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

Preorder.lift f = Preorder.mk (_ : ∀ (x : α), f x ≤ f x) (_ : ∀ (x x_1 x_2 : α), f x ≤ f x_1 → f x_1 ≤ f x_2 → f x ≤ f x_2)

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

PartialOrder α

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

Equations

PartialOrder.lift f inj = let src := Preorder.lift f; PartialOrder.mk (_ : ∀ (x x_1 : α), x ≤ x_1 → x_1 ≤ x → x = x_1)

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

Preorder (Subtype p)

Equations

Subtype.preorder p = Preorder.lift fun a => ↑a

instance Subtype.partialOrder {α : Type u} [inst : PartialOrder α] (p : α → Prop) :

PartialOrder (Subtype p)

Equations

Subtype.partialOrder p = PartialOrder.lift (fun a => ↑a) (_ : Function.Injective fun a => ↑a)

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

Subtype.decidableLE a b = h ↑a ↑b

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

Subtype.decidableLT a b = h ↑a ↑b

instance Subtype.linearOrder {α : Type u} [inst : LinearOrder α] (p : α → Prop) :

LinearOrder (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

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

Prod.instLEProd α β = { le := fun p q => p.fst ≤ q.fst ∧ p.snd ≤ q.snd }

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

Prod.swap x ≤ Prod.swap y ↔ x ≤ y

instance Prod.instPreorderProd (α : Type u) (β : Type v) [inst : Preorder α] [inst : Preorder β] :

Preorder (α × β)

Equations

Prod.instPreorderProd α β = let src := inferInstanceAs (LE (α × β)); Preorder.mk (_ : ∀ (x : α × β), x ≤ x) (_ : ∀ (x x_1 x_2 : α × β), x ≤ x_1 → x_1 ≤ x_2 → x ≤ x_2)

@[simp]

theorem Prod.swap_lt_swap {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {x : α × β} {y : α × β} :

Prod.swap x < Prod.swap y ↔ 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 β] :

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

Prod.instPartialOrderProd α β = let src := inferInstanceAs (Preorder (α × β)); PartialOrder.mk (_ : ∀ (x x_1 : α × β), x ≤ x_1 → x_1 ≤ x → x = x_1)

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 OrderDual.denselyOrdered (α : Type u) [inst : LT α] [h : DenselyOrdered α] :

DenselyOrdered αᵒᵈ

Equations

OrderDual.denselyOrdered = OrderDual.denselyOrdered.proof_1

@[simp]

theorem denselyOrdered_orderDual {α : Type u} [inst : LT α] :

DenselyOrdered αᵒᵈ ↔ DenselyOrdered α

instance instDenselyOrderedProdToLTInstPreorderProd {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] [inst : DenselyOrdered α] [inst : DenselyOrdered β] :

DenselyOrdered (α × β)

Equations

@instDenselyOrderedProdToLTInstPreorderProd = @instDenselyOrderedProdToLTInstPreorderProd.proof_1

instance instDenselyOrderedForAllToLTPreorder {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst : ∀ (i : ι), DenselyOrdered (α i)] :

DenselyOrdered ((i : ι) → α i)

Equations

@instDenselyOrderedForAllToLTPreorder = @instDenselyOrderedForAllToLTPreorder.proof_1

theorem le_of_forall_le_of_dense {α : Type u} [inst : LinearOrder α] [inst : DenselyOrdered α] {a₁ : α} {a₂ : α} (h : ∀ (a : α), a₂ < a → a₁ ≤ 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₂ < a → a₁ ≤ 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₁ < a → a₂ ≤ 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 < 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.

instance PUnit.linearOrder :

LinearOrder PUnit

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 PUnit.instDenselyOrderedPUnitToLTToPreorderToPartialOrderLinearOrder :

DenselyOrdered PUnit

Equations

PUnit.instDenselyOrderedPUnitToLTToPreorderToPartialOrderLinearOrder = PUnit.instDenselyOrderedPUnitToLTToPreorderToPartialOrderLinearOrder.proof_1

instance Prop.le :

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

Equations

Prop.le = { le := fun x x_1 => x → x_1 }

@[simp]

theorem le_Prop_eq :

(fun x x_1 => x ≤ x_1) = fun x x_1 => x → x_1

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

Subrelation r s ↔ r ≤ s

instance Prop.partialOrder :

PartialOrder Prop

Equations

Prop.partialOrder = let src := Prop.le; PartialOrder.mk Prop.partialOrder.proof_4

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

AsLinearOrder α = α

instance instInhabitedAsLinearOrder {α : Type u_1} [inst : Inhabited α] :

Inhabited (AsLinearOrder α)

Equations

instInhabitedAsLinearOrder = { default := default }

noncomputable instance AsLinearOrder.linearOrder {α : Type u_1} [inst : PartialOrder α] [inst : IsTotal α fun x x_1 => x ≤ x_1] :

LinearOrder (AsLinearOrder α)

Equations

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