Orders

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

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

@[deprecated]

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

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 α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : DecidableRel fun (x1 x2 : α) => x1 < x2

< is decidable if ≤ is.

Equations

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

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 α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : 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 : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (hab : a ≤ b) : a < b ∨ a = b

theorem Decidable.eq_or_lt_of_le {α : Type u_1} [PartialOrder α] {a b : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (hab : a ≤ b) : a = b ∨ a < b

theorem Decidable.le_iff_lt_or_eq {α : Type u_1} [PartialOrder α] {a b : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : 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