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 ≤ with a < b defined in the obvious way.

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

@[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 lt_iff_le_not_le {α : Type u_1} [Preorder α] {a b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem lt_of_le_not_le {α : 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 le_of_lt {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) : a ≤ b

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

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

theorem not_lt_of_le {α : 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) : ¬a < b

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

Alias of not_le_of_lt.

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

Alias of not_lt_of_le.

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

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

theorem gt_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_le_of_lt {α : Type u_1} [Preorder α] {a b c : α} (hab : a ≤ b) (hbc : b < c) : a < c

theorem gt_of_gt_of_ge {α : Type u_1} [Preorder α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c

theorem gt_of_ge_of_gt {α : Type u_1} [Preorder α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c

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

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

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 not_lt_of_lt {α : 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_eq_or_lt {α : Type u_1} [Preorder α] {a b : α} (h : a = b ∨ a < b) : a ≤ b

@[instance 900]

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

Equations

• instTransLe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransLt_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransLtLe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransLeLt_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGt_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGtGe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGeGt_mathlib = { trans := ⋯ }

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

< is decidable if ≤ is.

Equations

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

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.

Equations

• (a ⩿ b) = (a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b)

def «term_⩿_» : Lean.TrailingParserDescr

Notation for WCovBy 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: a < b and there is no element in between.

Equations

• (a ⋖ b) = (a < b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b)

def «term_⋖_» : Lean.TrailingParserDescr

Notation for CovBy 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_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b

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

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

Alias of le_antisymm.

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

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

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.eq_or_lt_of_le {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] (hab : a ≤ b) : a = b ∨ a < b

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

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

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