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.

Equations

• Preorder.mk' le_refl ge_trans lt_iff_le_not_ge = { toLE := inst✝¹, toLT := inst✝, le_refl := le_refl, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

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

Equations

• instTransLE = { trans := ⋯ }

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

Equations

• instTransLT = { trans := ⋯ }

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

Equations

• instTransLTLE = { trans := ⋯ }

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

Equations

• instTransLELT = { trans := ⋯ }

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

Equations

• instTransGE = { trans := ⋯ }

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

Equations

• instTransGT = { trans := ⋯ }

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

Equations

• instTransGTGE = { trans := ⋯ }

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

Equations

• instTransGEGT = { trans := ⋯ }

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

< is decidable if ≤ is.

Equations

• decidableLTOfDecidableLE x✝¹ x✝ = decidable_of_iff (x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹) ⋯

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.

Equations

• (a ⩿ b) = (a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < 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.

Equations

• «term_⩿_» = Lean.ParserDescr.trailingNode `«term_⩿_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⩿ ") (Lean.ParserDescr.cat `term 51))

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.

Equations

• (a ⋖ b) = (a < b ∧ ∀ ⦃c : α⦄, a < c → ¬c < 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.

Equations

• «term_⋖_» = Lean.ParserDescr.trailingNode `«term_⋖_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋖ ") (Lean.ParserDescr.cat `term 51))

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.

Equations

• PartialOrder.mk' le_antisymm = { toPreorder := inst✝, le_antisymm := ⋯ }

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.

Equations

• decidableEqOfDecidableLE x✝¹ x✝ = if hab : x✝¹ ≤ x✝ then if hba : x✝ ≤ x✝¹ then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

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