Orders

Defines classes for preorders and partial orders and proves some basic lemmas about them.

We also define covering relations on a preorder. We say that b covers a if a < b and there is no element in between. We say that b weakly covers a if a ≤ b and there is no element between a and b. In a partial order this is equivalent to a ⋖ b ∨ a = b, in a preorder this is equivalent to a ⋖ b ∨ (a ≤ b ∧ b ≤ a)

Notation

• a ⋖ b means that b covers a.
• a ⩿ b means that b weakly covers a.

Definition of Preorder and lemmas about types with a Preorder

class Preorder (α : Type u_2) extends LE α, LT α : Type u_2

A preorder is a reflexive, transitive relation ≤. In a preorder, a < b means a ≤ b ∧ ¬b ≤ a, and < is defined this way by default. You can override this definition to set a better def-eq.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a

def Preorder.mk' {α : Type u_1} [LE α] [LT α] (le_refl : ∀ (a : α), a ≤ a) (ge_trans : ∀ (a b c : α), b ≤ a → c ≤ b → c ≤ a) (lt_iff_le_not_ge : ∀ (a b : α), b < a ↔ b ≤ a ∧ ¬a ≤ b) : Preorder α

A variant of Preorder.mk which allows to_dual to dualize a Preorder instance.

instance instLawfulOrderLT_mathlib {α : Type u_1} [Preorder α] : Std.LawfulOrderLT α

instance instIsPreorder_mathlib {α : Type u_1} [Preorder α] : Std.IsPreorder α

@[simp]

theorem le_refl {α : Type u_1} [Preorder α] (a : α) : a ≤ a

The relation ≤ on a preorder is reflexive.

theorem le_rfl {α : Type u_1} [Preorder α] {a : α} : a ≤ a

A version of le_refl where the argument is implicit

theorem le_trans {α : Type u_1} [Preorder α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c

The relation ≤ on a preorder is transitive.

theorem ge_trans {α : Type u_1} [Preorder α] {a b c : α} : b ≤ a → c ≤ b → c ≤ a

theorem lt_iff_le_not_ge {α : Type u_1} [Preorder α] {a b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem lt_of_le_not_ge {α : Type u_1} [Preorder α] {a b : α} (hab : a ≤ b) (hba : ¬b ≤ a) : a < b

theorem le_of_eq {α : Type u_1} [Preorder α] {a b : α} (hab : a = b) : a ≤ b

theorem ge_of_eq {α : Type u_1} [Preorder α] {a b : α} (hab : a = b) : b ≤ a

theorem le_of_lt {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) : a ≤ b

theorem not_le_of_gt {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) : ¬b ≤ a

theorem not_lt_of_ge {α : Type u_1} [Preorder α] {a b : α} (hab : a ≤ b) : ¬b < a

theorem LT.lt.not_ge {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) : ¬b ≤ a

Alias of not_le_of_gt.

theorem LE.le.not_gt {α : Type u_1} [Preorder α] {a b : α} (hab : a ≤ b) : ¬b < a

Alias of not_lt_of_ge.

theorem lt_irrefl {α : Type u_1} [Preorder α] (a : α) : ¬a < a

theorem lt_of_lt_of_le {α : Type u_1} [Preorder α] {a b c : α} (hab : a < b) (hbc : b ≤ c) : a < c

theorem lt_of_lt_of_le' {α : Type u_1} [Preorder α] {a b c : α} (hab : b < a) (hbc : c ≤ b) : c < a

theorem lt_of_le_of_lt {α : Type u_1} [Preorder α] {a b c : α} (hab : a ≤ b) (hbc : b < c) : a < c

theorem lt_of_le_of_lt' {α : Type u_1} [Preorder α] {a b c : α} (hab : b ≤ a) (hbc : c < b) : c < a

theorem lt_trans {α : Type u_1} [Preorder α] {a b c : α} : a < b → b < c → a < c

theorem gt_trans {α : Type u_1} [Preorder α] {a b c : α} : b < a → c < b → c < a

theorem ne_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : a ≠ b

theorem ne_of_gt {α : Type u_1} [Preorder α] {a b : α} (h : b < a) : a ≠ b

theorem lt_asymm {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : ¬b < a

theorem not_lt_of_gt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : ¬b < a

Alias of lt_asymm.

theorem le_of_lt_or_eq {α : Type u_1} [Preorder α] {a b : α} (h : a < b ∨ a = b) : a ≤ b

theorem le_of_lt_or_eq' {α : Type u_1} [Preorder α] {a b : α} (h : b < a ∨ a = b) : b ≤ a

theorem le_of_eq_or_lt {α : Type u_1} [Preorder α] {a b : α} (h : a = b ∨ a < b) : a ≤ b

theorem le_of_eq_or_lt' {α : Type u_1} [Preorder α] {a b : α} (h : a = b ∨ b < a) : b ≤ a

instance instTransLE {α : Type u_1} [Preorder α] : Trans LE.le LE.le LE.le

instance instTransLT {α : Type u_1} [Preorder α] : Trans LT.lt LT.lt LT.lt

instance instTransLTLE {α : Type u_1} [Preorder α] : Trans LT.lt LE.le LT.lt

instance instTransLELT {α : Type u_1} [Preorder α] : Trans LE.le LT.lt LT.lt

instance instTransGE {α : Type u_1} [Preorder α] : Trans GE.ge GE.ge GE.ge

instance instTransGT {α : Type u_1} [Preorder α] : Trans GT.gt GT.gt GT.gt

instance instTransGTGE {α : Type u_1} [Preorder α] : Trans GT.gt GE.ge GT.gt

instance instTransGEGT {α : Type u_1} [Preorder α] : Trans GE.ge GT.gt GT.gt

def decidableLTOfDecidableLE {α : Type u_1} [Preorder α] [DecidableLE α] : DecidableLT α

< is decidable if ≤ is.

def WCovBy {α : Type u_1} [Preorder α] (a b : α) : Prop

WCovBy a b means that a = b or b covers a. This means that a ≤ b and there is no element in between. This is denoted a ⩿ b.

def «term_⩿_» : Lean.TrailingParserDescr

WCovBy a b means that a = b or b covers a. This means that a ≤ b and there is no element in between. This is denoted a ⩿ b.

def CovBy {α : Type u_2} [LT α] (a b : α) : Prop

CovBy a b means that b covers a. This means that a < b and there is no element in between. This is denoted a ⋖ b.

def «term_⋖_» : Lean.TrailingParserDescr

CovBy a b means that b covers a. This means that a < b and there is no element in between. This is denoted a ⋖ b.

Definition of PartialOrder and lemmas about types with a partial order

class PartialOrder (α : Type u_2) extends Preorder α : Type u_2

A partial order is a reflexive, transitive, antisymmetric relation ≤.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b

def PartialOrder.mk' {α : Type u_1} [Preorder α] (le_antisymm : ∀ (a b : α), b ≤ a → a ≤ b → a = b) : PartialOrder α

A variant of PartialOrder.mk which allows to_dual to dualize a PartialOrder instance.

instance instIsPartialOrder_mathlib {α : Type u_1} [PartialOrder α] : Std.IsPartialOrder α

theorem le_antisymm {α : Type u_1} [PartialOrder α] {a b : α} : a ≤ b → b ≤ a → a = b

theorem ge_antisymm {α : Type u_1} [PartialOrder α] {a b : α} : b ≤ a → a ≤ b → a = b

theorem eq_of_le_of_ge {α : Type u_1} [PartialOrder α] {a b : α} : a ≤ b → b ≤ a → a = b

Alias of le_antisymm.

theorem eq_of_ge_of_le {α : Type u_1} [PartialOrder α] {a b : α} : b ≤ a → a ≤ b → a = b

theorem le_antisymm_iff {α : Type u_1} [PartialOrder α] {a b : α} : a = b ↔ a ≤ b ∧ b ≤ a

theorem ge_antisymm_iff {α : Type u_1} [PartialOrder α] {a b : α} : a = b ↔ b ≤ a ∧ a ≤ b

theorem lt_of_le_of_ne {α : Type u_1} [PartialOrder α] {a b : α} : a ≤ b → a ≠ b → a < b

theorem lt_of_le_of_ne' {α : Type u_1} [PartialOrder α] {a b : α} : b ≤ a → a ≠ b → b < a

def decidableEqOfDecidableLE {α : Type u_1} [PartialOrder α] [DecidableLE α] : DecidableEq α

Equality is decidable if ≤ is.

theorem Decidable.lt_or_eq_of_le {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] (hab : a ≤ b) : a < b ∨ a = b

theorem Decidable.lt_or_eq_of_le' {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] (hab : b ≤ a) : b < a ∨ a = b

theorem Decidable.le_iff_lt_or_eq {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] : a ≤ b ↔ a < b ∨ a = b

theorem Decidable.le_iff_lt_or_eq' {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] : b ≤ a ↔ b < a ∨ a = b

theorem lt_or_eq_of_le {α : Type u_1} [PartialOrder α] {a b : α} : a ≤ b → a < b ∨ a = b

theorem lt_or_eq_of_le' {α : Type u_1} [PartialOrder α] {a b : α} : b ≤ a → b < a ∨ a = b

theorem le_iff_lt_or_eq {α : Type u_1} [PartialOrder α] {a b : α} : a ≤ b ↔ a < b ∨ a = b

theorem le_iff_lt_or_eq' {α : Type u_1} [PartialOrder α] {a b : α} : b ≤ a ↔ b < a ∨ a = b