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 α (≤).

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

a ≤ b → b ≤ a → b = a

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

a ≤ b → b ≠ a → a < b

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

a ≠ b → a ≤ b → a < b

theorem Ne.lt_of_le' {α : Type u} [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} [Preorder α] {a : α} {b : α} {c : α} :

a ≤ b → b ≤ c → a ≤ c

Alias of le_trans.

The relation ≤ on a preorder is transitive.

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

b ≤ c → a ≤ b → a ≤ c

Alias of le_trans'.

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

a ≤ b → b < c → a < c

Alias of lt_of_le_of_lt.

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

b ≤ c → a < b → a < c

Alias of lt_of_le_of_lt'.

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

a ≤ b → b ≤ a → a = b

Alias of le_antisymm.

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

a ≤ b → b ≤ a → b = a

Alias of ge_antisymm.

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

a ≤ b → a ≠ b → a < b

Alias of lt_of_le_of_ne.

theorem LE.le.lt_of_ne' {α : Type u} [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} [Preorder α] {a : α} {b : α} :

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

Alias of lt_of_le_not_le.

theorem LE.le.lt_or_eq {α : Type u} [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} [PartialOrder α] [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} [Preorder α] {a : α} {b : α} :

a < b → a ≤ b

Alias of le_of_lt.

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

a < b → b < c → a < c

Alias of lt_trans.

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

b < c → a < b → a < c

Alias of lt_trans'.

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

a < b → b ≤ c → a < c

Alias of lt_of_lt_of_le.

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

b < c → a ≤ b → a < c

Alias of lt_of_lt_of_le'.

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

a ≠ b

Alias of ne_of_lt.

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

¬b < a

Alias of lt_asymm.

theorem 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 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 LE.le.trans_eq' {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

b ≤ c → a = b → a ≤ c

Alias of le_of_le_of_eq'.

theorem 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 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'.

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

@[simp]

theorem le_of_subsingleton {α : Type u} [Preorder α] {a : α} {b : α} [Subsingleton α] :

a ≤ b

theorem not_lt_of_subsingleton {α : Type u} [Preorder α] {a : α} {b : α} [Subsingleton α] :

¬a < b

theorem LE.le.ge {α : Type u} [LE α] {x : α} {y : α} (h : x ≤ y) :

y ≥ x

theorem LE.le.lt_iff_ne {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

a < b ↔ a ≠ b

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

a < b ↔ b ≠ a

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

¬a < b ↔ a = b

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

¬a < b ↔ b = a

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

b ≤ a ↔ b = a

theorem LE.le.ge_iff_eq {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

b ≤ a ↔ a = b

theorem LE.le.lt_or_le {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (c : α) :

a < c ∨ c ≤ b

theorem LE.le.le_or_lt {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (c : α) :

a ≤ c ∨ c < b

theorem LE.le.le_or_le {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (c : α) :

a ≤ c ∨ c ≤ b

theorem LT.lt.gt {α : Type u} [LT α] {x : α} {y : α} (h : x < y) :

y > x

theorem LT.lt.false {α : Type u} [Preorder α] {x : α} :

x < x → False

theorem LT.lt.ne' {α : Type u} [Preorder α] {x : α} {y : α} (h : x < y) :

y ≠ x

theorem LT.lt.lt_or_lt {α : Type u} [LinearOrder α] {x : α} {y : α} (h : x < y) (z : α) :

x < z ∨ z < y

theorem GE.ge.le {α : Type u} [LE α] {x : α} {y : α} (h : x ≥ y) :

y ≤ x

theorem GT.gt.lt {α : Type u} [LT α] {x : α} {y : α} (h : x > y) :

y < x

theorem ge_of_eq {α : Type u} [Preorder α] {a : α} {b : α} (h : a = b) :

a ≥ b

@[simp]

theorem ge_iff_le {α : Type u} [LE α] {a : α} {b : α} :

a ≥ b ↔ b ≤ a

@[simp]

theorem gt_iff_lt {α : Type u} [LT α] {a : α} {b : α} :

a > b ↔ b < a

theorem not_le_of_lt {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) :

theorem 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 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

theorem Decidable.le_iff_eq_or_lt {α : Type u} [PartialOrder α] [DecidableRel fun x x_1 => x ≤ x_1] {a : α} {b : α} :

a ≤ b ↔ a = b ∨ a < b

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

a ≤ b ↔ a = b ∨ a < b

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

a < b ↔ a ≤ b ∧ a ≠ b

theorem eq_iff_not_lt_of_le {α : Type u_3} [PartialOrder α] {x : α} {y : α} :

x ≤ y → y = x ↔ ¬x < y

theorem Decidable.eq_iff_le_not_lt {α : Type u} [PartialOrder α] [DecidableRel fun x x_1 => x ≤ x_1] {a : α} {b : α} :

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

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

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

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

a = b ∨ a < b

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

b = a ∨ a < b

theorem gt_or_eq_of_le {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

a < b ∨ b = a

theorem LE.le.eq_or_lt_dec {α : Type u} [PartialOrder α] [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} [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} [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} [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} [PartialOrder α] {a : α} {b : α} (hab : a ≤ b) (hba : ¬a < b) :

a = b

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

b = a

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

a ≤ b ↔ a < b

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

¬a ≤ b ∨ ¬b ≤ a

theorem Decidable.ne_iff_lt_iff_le {α : Type u} [PartialOrder α] [DecidableEq α] {a : α} {b : α} :

(a ≠ b ↔ a < b) ↔ a ≤ b

@[simp]

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

(a ≠ b ↔ a < b) ↔ a ≤ b

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

min a b = if b ≤ a then b else a

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

max a b = if b ≤ a then a else b

theorem lt_of_not_le {α : Type u} [LinearOrder α] {a : α} {b : α} (h : ¬b ≤ a) :

a < b

theorem lt_iff_not_le {α : Type u} [LinearOrder α] {x : α} {y : α} :

x < y ↔ ¬y ≤ x

theorem Ne.lt_or_lt {α : Type u} [LinearOrder α] {x : α} {y : α} (h : x ≠ y) :

x < y ∨ y < x

@[simp]

theorem lt_or_lt_iff_ne {α : Type u} [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} [LinearOrder α] {a : α} {b : α} :

¬a < b ↔ a = b ∨ b < a

theorem exists_ge_of_linear {α : Type u} [LinearOrder α] (a : α) (b : α) :

∃ c, a ≤ c ∧ b ≤ c

theorem lt_imp_lt_of_le_imp_le {α : Type u} {β : Type u_3} [LinearOrder α] [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_3} [LinearOrder α] [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_3} [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_3} [LinearOrder α] [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_3} [LinearOrder α] [LinearOrder β] {a : α} {b : α} {c : β} {d : β} :

(a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c)

theorem eq_of_forall_le_iff {α : Type u} [PartialOrder α] {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} [LinearOrder α] {a : α} {b : α} (H : ∀ (c : α), c < a → c < b) :

a ≤ b

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

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

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

b ≤ a

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

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

theorem eq_of_forall_ge_iff {α : Type u} [PartialOrder α] {a : α} {b : α} (H : ∀ (c : α), a ≤ c ↔ b ≤ c) :

a = b

theorem eq_of_forall_lt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} (h : ∀ (c : α), c < a ↔ c < b) :

a = b

theorem eq_of_forall_gt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} (h : ∀ (c : α), a < c ↔ b < c) :

a = b

theorem rel_imp_eq_of_rel_imp_le {α : Type u} {β : Type v} [PartialOrder β] (r : α → α → Prop) [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 : α} [Preorder α] (hca : c ≤ a) (hbd : b ≤ d) :

a ≤ b → c ≤ d

monotonicity of ≤ with respect to →

theorem commutative_of_le {α : Type u} {β : Type v} [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} [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_3} :

Function.Injective (@Preorder.toLE α)

theorem PartialOrder.toPreorder_injective {α : Type u_3} :

Function.Injective (@PartialOrder.toPreorder α)

theorem LinearOrder.toPartialOrder_injective {α : Type u_3} :

Function.Injective (@LinearOrder.toPartialOrder α)

theorem Preorder.ext {α : Type u_3} {A : Preorder α} {B : Preorder α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

theorem PartialOrder.ext {α : Type u_3} {A : PartialOrder α} {B : PartialOrder α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

theorem LinearOrder.ext {α : Type u_3} {A : LinearOrder α} {B : LinearOrder α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

def Order.Preimage {α : Sort u_3} {β : Sort u_4} (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).

Instances For

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

Instances For

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

DecidableRel (f ⁻¹'o s)

The preimage of a decidable order is decidable.

Order dual #

def OrderDual (α : Type u_3) :

Type u_3

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

Instances For

def «term_ᵒᵈ» :

Lean.TrailingParserDescr

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

Instances For

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

Nonempty αᵒᵈ

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

Subsingleton αᵒᵈ

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

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

instance OrderDual.instPreorder (α : Type u_3) [Preorder α] :

Preorder αᵒᵈ

instance OrderDual.instPartialOrder (α : Type u_3) [PartialOrder α] :

PartialOrder αᵒᵈ

instance OrderDual.instLinearOrder (α : Type u_3) [LinearOrder α] :

LinearOrder αᵒᵈ

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

Inhabited αᵒᵈ

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

OrderDual.instPreorder αᵒᵈ = H

theorem OrderDual.instPartialOrder.dual_dual (α : Type u_3) [H : PartialOrder α] :

OrderDual.instPartialOrder αᵒᵈ = H

theorem OrderDual.instLinearOrder.dual_dual (α : Type u_3) [H : LinearOrder α] :

OrderDual.instLinearOrder αᵒᵈ = H

`HasCompl` #

class HasCompl (α : Type u_3) :

Type u_3

compl : α → α
Set / lattice complement

Set / lattice complement

Instances

def «term_ᶜ» :

Lean.TrailingParserDescr

Set / lattice complement

Instances For

instance Prop.hasCompl :

instance Pi.hasCompl {ι : Type u} {α : ι → Type v} [(i : ι) → HasCompl (α i)] :

HasCompl ((i : ι) → α i)

theorem Pi.compl_def {ι : Type u} {α : ι → Type v} [(i : ι) → HasCompl (α i)] (x : (i : ι) → α i) :

xᶜ = fun i => (x i)ᶜ

@[simp]

theorem Pi.compl_apply {ι : Type u} {α : ι → Type v} [(i : ι) → HasCompl (α i)] (x : (i : ι) → α i) (i : ι) :

((i : ι) → α i)ᶜ Pi.hasCompl x i = (x i)ᶜ

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

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

IsIrrefl α rᶜ

Order instances on the function space #

instance Pi.hasLe {ι : Type u} {α : ι → Type v} [(i : ι) → LE (α i)] :

LE ((i : ι) → α i)

theorem Pi.le_def {ι : Type u} {α : ι → Type v} [(i : ι) → LE (α i)] {x : (i : ι) → α i} {y : (i : ι) → α i} :

x ≤ y ↔ ∀ (i : ι), x i ≤ y i

instance Pi.preorder {ι : Type u} {α : ι → Type v} [(i : ι) → Preorder (α i)] :

Preorder ((i : ι) → α i)

theorem Pi.lt_def {ι : Type u} {α : ι → Type v} [(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} [(i : ι) → PartialOrder (π i)] :

PartialOrder ((i : ι) → π i)

def StrongLT {ι : Type u_1} {π : ι → Type u_2} [(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.

Instances For

theorem le_of_strongLT {ι : Type u_1} {π : ι → Type u_2} [(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} [(i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} [Nonempty ι] (h : StrongLT a b) :

a < b

theorem strongLT_of_strongLT_of_le {ι : Type u_1} {π : ι → Type u_2} [(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} [(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} [(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} [(i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} [Nonempty ι] (h : StrongLT a b) :

a < b

Alias of lt_of_strongLT.

theorem StrongLT.trans_le {ι : Type u_1} {π : ι → Type u_2} [(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} [(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} [DecidableEq ι] [(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} [DecidableEq ι] [(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} [DecidableEq ι] [(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 update_le_update_iff' {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} {b : π i} :

Function.update x i a ≤ Function.update x i b ↔ a ≤ b

@[simp]

theorem update_lt_update_iff {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} {b : π i} :

Function.update x i a < Function.update x i b ↔ a < b

@[simp]

theorem le_update_self_iff {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] [(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} [DecidableEq ι] [(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} [DecidableEq ι] [(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} [DecidableEq ι] [(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} [(i : ι) → SDiff (α i)] :

SDiff ((i : ι) → α i)

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

p (min x y)

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

p (max x y)

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

p (min x y)

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

p (max x y)

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

min x y = if x < y then x else y

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

max x y = if x < y then y else x

`Sup` and `Inf` #

theorem Sup.ext {α : Type u} (x : Sup α) (y : Sup α) (sup : Sup.sup = Sup.sup) :

x = y

theorem Sup.ext_iff {α : Type u} (x : Sup α) (y : Sup α) :

x = y ↔ Sup.sup = Sup.sup

class Sup (α : Type u) :

sup : α → α → α
Least upper bound (\lub notation)

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

inf : α → α → α
Greatest lower bound (\glb notation)

Typeclass for the ⊓ (\glb) notation

Instances

def «term_⊔_» :

Lean.TrailingParserDescr

Least upper bound (\lub notation)

Instances For

def «term_⊓_» :

Lean.TrailingParserDescr

Greatest lower bound (\glb notation)

Instances For

Lifts of order instances #

@[reducible]

def Preorder.lift {α : Type u_3} {β : Type u_4} [Preorder β] (f : α → β) :

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

Instances For

@[reducible]

def PartialOrder.lift {α : Type u_3} {β : Type u_4} [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].

Instances For

theorem compare_of_injective_eq_compareOfLessAndEq {α : Type u} {β : Type v} (a : α) (b : α) [LinearOrder β] [DecidableEq α] (f : α → β) (inj : Function.Injective f) [Decidable (a < b)] :

compare (f a) (f b) = compareOfLessAndEq a b

@[reducible]

def LinearOrder.lift {α : Type u_3} {β : Type u_4} [LinearOrder β] [Sup α] [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].

Instances For

@[reducible]

def LinearOrder.lift' {α : Type u_3} {β : Type u_4} [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].

Instances For

@[reducible]

def LinearOrder.liftWithOrd {α : Type u_3} {β : Type u_4} [LinearOrder β] [Sup α] [Inf α] [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].

Instances For

@[reducible]

def LinearOrder.liftWithOrd' {α : Type u_3} {β : Type u_4} [LinearOrder β] [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].

Instances For

Subtype of an order #

instance Subtype.le {α : Type u} [LE α] {p : α → Prop} :

instance Subtype.lt {α : Type u} [LT α] {p : α → Prop} :

@[simp]

theorem Subtype.mk_le_mk {α : Type u} [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} [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} [LE α] {p : α → Prop} {x : Subtype p} {y : Subtype p} :

↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem Subtype.coe_lt_coe {α : Type u} [LT α] {p : α → Prop} {x : Subtype p} {y : Subtype p} :

↑x < ↑y ↔ x < y

instance Subtype.preorder {α : Type u} [Preorder α] (p : α → Prop) :

Preorder (Subtype p)

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

PartialOrder (Subtype p)

instance Subtype.decidableLE {α : Type u} [Preorder α] [h : DecidableRel fun x x_1 => x ≤ x_1] {p : α → Prop} :

DecidableRel fun x x_1 => x ≤ x_1

instance Subtype.decidableLT {α : Type u} [Preorder α] [h : DecidableRel fun x x_1 => x < x_1] {p : α → Prop} :

DecidableRel fun x x_1 => x < x_1

instance Subtype.linearOrder {α : Type u} [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.

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) [LE α] [LE β] :

LE (α × β)

instance Prod.instDecidableLE (α : Type u) (β : Type v) [LE α] [LE β] (x : α × β) (y : α × β) [Decidable (x.fst ≤ y.fst)] [Decidable (x.snd ≤ y.snd)] :

Decidable (x ≤ y)

theorem Prod.le_def {α : Type u} {β : Type v} [LE α] [LE β] {x : α × β} {y : α × β} :

x ≤ y ↔ x.fst ≤ y.fst ∧ x.snd ≤ y.snd

@[simp]

theorem Prod.mk_le_mk {α : Type u} {β : Type v} [LE α] [LE β] {x₁ : α} {x₂ : α} {y₁ : β} {y₂ : β} :

(x₁, y₁) ≤ (x₂, y₂) ↔ x₁ ≤ x₂ ∧ y₁ ≤ y₂

@[simp]

theorem Prod.swap_le_swap {α : Type u} {β : Type v} [LE α] [LE β] {x : α × β} {y : α × β} :

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

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

Preorder (α × β)

@[simp]

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

Prod.swap x < Prod.swap y ↔ 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₂

instance Prod.instPartialOrder (α : Type u) (β : Type v) [PartialOrder α] [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 α ×ₗ β = α × β.)

Additional order classes #

class DenselyOrdered (α : Type u) [LT α] :

dense : ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
An order is dense if there is an element between any pair of distinct elements.

An order is dense if there is an element between any pair of distinct comparable elements.

Instances

theorem exists_between {α : Type u} [LT α] [DenselyOrdered α] {a₁ : α} {a₂ : α} :

a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

instance OrderDual.denselyOrdered (α : Type u) [LT α] [h : DenselyOrdered α] :

DenselyOrdered αᵒᵈ

@[simp]

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

DenselyOrdered αᵒᵈ ↔ DenselyOrdered α

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

DenselyOrdered (α × β)

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

DenselyOrdered ((i : ι) → α i)

theorem le_of_forall_le_of_dense {α : Type u} [LinearOrder α] [DenselyOrdered α] {a₁ : α} {a₂ : α} (h : ∀ (a : α), a₂ < a → a₁ ≤ a) :

a₁ ≤ a₂

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

a₁ = a₂

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

a₁ ≤ a₂

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

a₁ = a₂

theorem dense_or_discrete {α : Type u} [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} [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.{u_3 + 1}

theorem PUnit.max_eq (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) :

max a b = PUnit.unit

theorem PUnit.min_eq (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) :

min a b = PUnit.unit

theorem PUnit.le (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) :

a ≤ b

theorem PUnit.not_lt (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) :

¬a < b

instance PUnit.instDenselyOrderedPUnitToLTToPreorderToPartialOrderLinearOrder :

DenselyOrdered PUnit.{u_3 + 1}

instance Prop.le :

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

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

Linear order from a total partial order #

def AsLinearOrder (α : Type u) :

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

Instances For

instance instInhabitedAsLinearOrder {α : Type u_3} [Inhabited α] :

Inhabited (AsLinearOrder α)

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

LinearOrder (AsLinearOrder α)