Documentation

Mathlib.Order.Defs.PartialOrder

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

Instances

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

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

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 α] :

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

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

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

Instances

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 α] :

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