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

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

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

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

theorem Preorder.le_trans {α : Type u} [self : Preorder α] (a : α) (b : α) (c : α) : a ≤ b → b ≤ c → a ≤ c

theorem Preorder.lt_iff_le_not_le {α : Type u} [self : Preorder α] (a : α) (b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a

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

The relation ≤ on a preorder is reflexive.

theorem le_rfl {α : Type u} [Preorder α] {a : α} : a ≤ a

A version of le_refl where the argument is implicit

theorem le_trans {α : Type u} [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} [Preorder α] {a : α} {b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[instance 900]

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

Equations

• instTransLe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransLt_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransLtLe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransLeLt_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGt_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGtGe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGeGt_mathlib = { trans := ⋯ }

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

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

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

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

def decidableLTOfDecidableLE {α : Type u} [Preorder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] : DecidableRel fun (x x_1 : α) => x < x_1

< is decidable if ≤ is.

Equations

• decidableLTOfDecidableLE x✝ x = match x✝, x with | a, b => if hab : a ≤ b then if hba : b ≤ a then isFalse ⋯ else isTrue ⋯ else isFalse ⋯

Definition of PartialOrder and lemmas about types with a partial order

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

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 PartialOrder.le_antisymm {α : Type u} [self : PartialOrder α] (a : α) (b : α) : a ≤ b → b ≤ a → a = b

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

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

Alias of le_antisymm.

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

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

def decidableEqOfDecidableLE {α : Type u} [PartialOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] : DecidableEq α

Equality is decidable if ≤ is.

Equations

• decidableEqOfDecidableLE x✝ x = match x✝, x with | a, b => if hab : a ≤ b then if hba : b ≤ a then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

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

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

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

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

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

Definition of LinearOrder and lemmas about types with a linear order

def maxDefault {α : Type u} [LE α] [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

def minDefault {α : Type u} [LE α] [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

def tacticCompareOfLessAndEq_rfl : Lean.ParserDescr

This attempts to prove that a given instance of compare is equal to compareOfLessAndEq by introducing the arguments and trying the following approaches in order:

1. seeing if rfl works
2. seeing if the compare at hand is nonetheless essentially compareOfLessAndEq, but, because of implicit arguments, requires us to unfold the defs and split the ifs in the definition of compareOfLessAndEq
3. seeing if we can split by cases on the arguments, then see if the defs work themselves out (useful when compare is defined via a match statement, as it is for Bool)

Equations

• tacticCompareOfLessAndEq_rfl = Lean.ParserDescr.node `tacticCompareOfLessAndEq_rfl 1024 (Lean.ParserDescr.nonReservedSymbol "compareOfLessAndEq_rfl" false)

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

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

• 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
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

  A linear order is total.

• decidableLE : DecidableRel fun (x x_1 : α) => x ≤ x_1

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

• decidableEq : DecidableEq α

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

• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1

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

• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b

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

• max_def : ∀ (a b : α), max a b = if a ≤ b then b else a

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

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b

  Comparison via compare is equal to the canonical comparison given decidable < and =.

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

A linear order is total.

theorem LinearOrder.min_def {α : Type u} [self : LinearOrder α] (a : α) (b : α) : min a b = if a ≤ b then a else b

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

theorem LinearOrder.max_def {α : Type u} [self : LinearOrder α] (a : α) (b : α) : max a b = if a ≤ b then b else a

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

theorem LinearOrder.compare_eq_compareOfLessAndEq {α : Type u} [self : LinearOrder α] (a : α) (b : α) : compare a b = compareOfLessAndEq a b

Comparison via compare is equal to the canonical comparison given decidable < and =.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[instance 900]

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

Equations

• instDecidableLt_mathlib a b = LinearOrder.decidableLT a b

@[instance 900]

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

Equations

• instDecidableLe_mathlib a b = LinearOrder.decidableLE a b

@[instance 900]

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

Equations

• instDecidableEq_mathlib a b = LinearOrder.decidableEq a b

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

instance instIsTotalPreorderLe {α : Type u} [LinearOrder α] : IsTotalPreorder α fun (x x_1 : α) => x ≤ x_1

Equations

• ⋯ = ⋯

instance isStrictWeakOrder_of_linearOrder {α : Type u} [LinearOrder α] : IsStrictWeakOrder α fun (x x_1 : α) => x < x_1

Equations

• ⋯ = ⋯

instance isStrictTotalOrder_of_linearOrder {α : Type u} [LinearOrder α] : IsStrictTotalOrder α fun (x x_1 : α) => x < x_1

Equations

• ⋯ = ⋯

def ltByCases {α : Type u} [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

• ltByCases x y h₁ h₂ h₃ = if h : x < y then h₁ h else if h' : y < x then h₃ h' else h₂ ⋯

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

theorem compare_lt_iff_lt {α : Type u} [LinearOrder α] {a : α} {b : α} : compare a b = Ordering.lt ↔ a < b

theorem compare_gt_iff_gt {α : Type u} [LinearOrder α] {a : α} {b : α} : compare a b = Ordering.gt ↔ a > b

theorem compare_eq_iff_eq {α : Type u} [LinearOrder α] {a : α} {b : α} : compare a b = Ordering.eq ↔ a = b

theorem compare_le_iff_le {α : Type u} [LinearOrder α] {a : α} {b : α} : compare a b ≠ Ordering.gt ↔ a ≤ b

theorem compare_ge_iff_ge {α : Type u} [LinearOrder α] {a : α} {b : α} : compare a b ≠ Ordering.lt ↔ a ≥ b

theorem compare_iff {α : Type u} [LinearOrder α] (a : α) (b : α) {o : Ordering} : compare a b = o ↔ o.toRel a b

instance instTransCmpCompare_mathlib {α : Type u} [LinearOrder α] : Batteries.TransCmp compare

Equations

• ⋯ = ⋯