Orders

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

Definition of Preorder and lemmas about types with a Preorder

ink

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

• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : autoParam (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) _auto✝

A preorder is a reflexive, transitive relation ≤≤ with a < b defined in the obvious way.

ink

@[simp]

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

The relation ≤≤ on a preorder is reflexive.

ink

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

The relation ≤≤ on a preorder is transitive.

ink

theorem lt_iff_le_not_le {α : Type u} [inst : Preorder α] {a : α} {b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a

ink

theorem lt_of_le_not_le {α : Type u} [inst : Preorder α] {a : α} {b : α} : a ≤ b → ¬b ≤ a → a < b

ink

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

ink

theorem le_of_eq {α : Type u} [inst : Preorder α] {a : α} {b : α} : a = b → a ≤ b

ink

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

ink

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

ink

theorem gt_irrefl {α : Type u} [inst : Preorder α] (a : α) : ¬a > a

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem le_of_lt {α : Type u} [inst : Preorder α] {a : α} {b : α} : a < b → a ≤ b

ink

theorem lt_of_lt_of_le {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} : a < b → b ≤ c → a < c

ink

theorem lt_of_le_of_lt {α : Type u} [inst : Preorder α] {a : α} {b : α} {c : α} : a ≤ b → b < c → a < c

ink

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

ink

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

ink

instance instTransLeToLE {α : Type u} [inst : Preorder α] : Trans LE.le LE.le LE.le

Equations

• instTransLeToLE = { trans := (_ : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c) }

ink

instance instTransLtToLT {α : Type u} [inst : Preorder α] : Trans LT.lt LT.lt LT.lt

Equations

• instTransLtToLT = { trans := (_ : ∀ {a b c : α}, a < b → b < c → a < c) }

ink

instance instTransLtToLTLeToLE {α : Type u} [inst : Preorder α] : Trans LT.lt LE.le LT.lt

Equations

• instTransLtToLTLeToLE = { trans := (_ : ∀ {a b c : α}, a < b → b ≤ c → a < c) }

ink

instance instTransLeToLELtToLT {α : Type u} [inst : Preorder α] : Trans LE.le LT.lt LT.lt

Equations

• instTransLeToLELtToLT = { trans := (_ : ∀ {a b c : α}, a ≤ b → b < c → a < c) }

ink

instance instTransGeToLE {α : Type u} [inst : Preorder α] : Trans GE.ge GE.ge GE.ge

Equations

• instTransGeToLE = { trans := (_ : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c) }

ink

instance instTransGtToLT {α : Type u} [inst : Preorder α] : Trans GT.gt GT.gt GT.gt

Equations

• instTransGtToLT = { trans := (_ : ∀ {a b c : α}, a > b → b > c → a > c) }

ink

instance instTransGtToLTGeToLE {α : Type u} [inst : Preorder α] : Trans GT.gt GE.ge GT.gt

Equations

• instTransGtToLTGeToLE = { trans := (_ : ∀ {a b c : α}, a > b → b ≥ c → a > c) }

ink

instance instTransGeToLEGtToLT {α : Type u} [inst : Preorder α] : Trans GE.ge GT.gt GT.gt

Equations

• instTransGeToLEGtToLT = { trans := (_ : ∀ {a b c : α}, a ≥ b → b > c → a > c) }

ink

theorem not_le_of_gt {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a > b) : ¬a ≤ b

ink

theorem not_lt_of_ge {α : Type u} [inst : Preorder α] {a : α} {b : α} (h : a ≥ b) : ¬a < b

ink

theorem le_of_lt_or_eq {α : Type u} [inst : Preorder α] {a : α} {b : α} : a < b ∨ a = b → a ≤ b

ink

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

ink

instance decidableLT_of_decidableLE {α : Type u} [inst : Preorder α] [inst : DecidableRel fun x x_1 => x ≤ x_1] : DecidableRel fun x x_1 => x < x_1

Equations

• One or more equations did not get rendered due to their size.

Definition of PartialOrder and lemmas about types with a partial order

ink

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

• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b

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

ink

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

ink

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

ink

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

ink

instance decidableEq_of_decidableLE {α : Type u} [inst : PartialOrder α] [inst : DecidableRel fun x x_1 => x ≤ x_1] : DecidableEq α

Equations

• decidableEq_of_decidableLE x x = match x, x with | a, b => if hab : a ≤ b then if hba : b ≤ a then isTrue (_ : a = b) else isFalse (_ : a = b → False) else isFalse (_ : a = b → False)

ink

theorem Decidable.lt_or_eq_of_le {α : Type u} [inst : PartialOrder α] [inst : DecidableRel fun x x_1 => x ≤ x_1] {a : α} {b : α} (hab : a ≤ b) : a < b ∨ a = b

ink

theorem Decidable.eq_or_lt_of_le {α : Type u} [inst : PartialOrder α] [inst : DecidableRel fun x x_1 => x ≤ x_1] {a : α} {b : α} (hab : a ≤ b) : a = b ∨ a < b

ink

theorem Decidable.le_iff_lt_or_eq {α : Type u} [inst : PartialOrder α] [inst : DecidableRel fun x x_1 => x ≤ x_1] {a : α} {b : α} : a ≤ b ↔ a < b ∨ a = b

ink

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

ink

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

Definition of LinearOrder and lemmas about types with a linear order

ink

def maxDefault {α : Type u} [inst : LE α] [inst : DecidableRel fun x x_1 => x ≤ x_1] (a : α) (b : α) : α

Default definition of max.

Equations

• maxDefault a b = if a ≤ b then b else a

ink

def minDefault {α : Type u} [inst : LE α] [inst : DecidableRel fun x x_1 => x ≤ x_1] (a : α) (b : α) : α

Default definition of min.

Equations

• minDefault a b = if a ≤ b then a else b

ink

class LinearOrder (α : Type u) extends PartialOrder , Min , Max : Type u

• A linear order is total.

  le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_le : DecidableRel fun x x_1 => x ≤ x_1

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_eq : DecidableEq α

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_lt : DecidableRel fun x x_1 => x < x_1

• The minimum function is equivalent to the one you get from minOfLe.

  min_def : autoParam (∀ (a b : α), min a b = if a ≤ b then a else b) _auto✝

• The minimum function is equivalent to the one you get from maxOfLe.

  max_def : autoParam (∀ (a b : α), max a b = if a ≤ b then b else a) _auto✝

A linear order is reflexive, transitive, antisymmetric and total relation ≤≤. We assume that every linear ordered type has decidable (≤)≤), (<), and (=).

ink

theorem le_total {α : Type u} [inst : LinearOrder α] (a : α) (b : α) : a ≤ b ∨ b ≤ a

ink

theorem le_of_not_ge {α : Type u} [inst : LinearOrder α] {a : α} {b : α} : ¬a ≥ b → a ≤ b

ink

theorem le_of_not_le {α : Type u} [inst : LinearOrder α] {a : α} {b : α} : ¬a ≤ b → b ≤ a

ink

theorem not_lt_of_gt {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : a > b) : ¬a < b

ink

theorem lt_trichotomy {α : Type u} [inst : LinearOrder α] (a : α) (b : α) : a < b ∨ a = b ∨ b < a

ink

theorem le_of_not_lt {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : ¬b < a) : a ≤ b

ink

theorem le_of_not_gt {α : Type u} [inst : LinearOrder α] {a : α} {b : α} : ¬a > b → a ≤ b

ink

theorem lt_of_not_ge {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : ¬a ≥ b) : a < b

ink

theorem lt_or_le {α : Type u} [inst : LinearOrder α] (a : α) (b : α) : a < b ∨ b ≤ a

ink

theorem le_or_lt {α : Type u} [inst : LinearOrder α] (a : α) (b : α) : a ≤ b ∨ b < a

ink

theorem lt_or_ge {α : Type u} [inst : LinearOrder α] (a : α) (b : α) : a < b ∨ a ≥ b

ink

theorem le_or_gt {α : Type u} [inst : LinearOrder α] (a : α) (b : α) : a ≤ b ∨ a > b

ink

theorem lt_or_gt_of_ne {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : a ≠ b) : a < b ∨ a > b

ink

theorem ne_iff_lt_or_gt {α : Type u} [inst : LinearOrder α] {a : α} {b : α} : a ≠ b ↔ a < b ∨ a > b

ink

theorem lt_iff_not_ge {α : Type u} [inst : LinearOrder α] (x : α) (y : α) : x < y ↔ ¬x ≥ y

ink

@[simp]

theorem not_lt {α : Type u} [inst : LinearOrder α] {a : α} {b : α} : ¬a < b ↔ b ≤ a

ink

@[simp]

theorem not_le {α : Type u} [inst : LinearOrder α] {a : α} {b : α} : ¬a ≤ b ↔ b < a

ink

instance instDecidableLtToLTToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] (a : α) (b : α) : Decidable (a < b)

Equations

• instDecidableLtToLTToPreorderToPartialOrder a b = LinearOrder.decidable_lt a b

ink

instance instDecidableLeToLEToPreorderToPartialOrder {α : Type u} [inst : LinearOrder α] (a : α) (b : α) : Decidable (a ≤ b)

Equations

• instDecidableLeToLEToPreorderToPartialOrder a b = LinearOrder.decidable_le a b

ink

instance instDecidableEq {α : Type u} [inst : LinearOrder α] (a : α) (b : α) : Decidable (a = b)

Equations

• instDecidableEq a b = LinearOrder.decidable_eq a b

ink

theorem eq_or_lt_of_not_lt {α : Type u} [inst : LinearOrder α] {a : α} {b : α} (h : ¬a < b) : a = b ∨ b < a

ink

def lt_by_cases {α : Type u} [inst : LinearOrder α] (x : α) (y : α) {P : Sort u_1} (h₁ : x < y → P) (h₂ : x = y → P) (h₃ : y < x → P) : P

Perform a case-split on the ordering of x and y in a decidable linear order.

Equations

• lt_by_cases x y h₁ h₂ h₃ = if h : x < y then h₁ h else if h' : y < x then h₃ h' else h₂ (_ : x = y)

ink

theorem le_imp_le_of_lt_imp_lt {α : Type u} {β : Type u_1} [inst : Preorder α] [inst : LinearOrder β] {a : α} {b : α} {c : β} {d : β} (H : d < c → b < a) (h : a ≤ b) : c ≤ d