Orders

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

Definition of LinearOrder and lemmas about types with a linear order

def maxDefault {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (a b : α) : α

Default definition of max.

Equations

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

def minDefault {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (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_2) extends PartialOrder α, Min α, Max α, Ord α : Type u_2

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

  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 (x1 x2 : α) => x1 < x2

  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 le_total {α : Type u_1} [LinearOrder α] (a b : α) : a ≤ b ∨ b ≤ a

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[instance 900]

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

Equations

• instDecidableLt_mathlib a b = LinearOrder.decidableLT a b

@[instance 900]

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

Equations

• instDecidableLe_mathlib a b = LinearOrder.decidableLE a b

@[instance 900]

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

Equations

• instDecidableEq_mathlib a b = LinearOrder.decidableEq a b

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

def ltByCases {α : Type u_1} [LinearOrder α] (x y : α) {P : Sort u_2} (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₂ ⋯

Deprecated properties of inequality on Nat

@[deprecated]

def Nat.ltGeByCases {a b : Nat} {C : Sort u_2} (h₁ : a < b → C) (h₂ : b ≤ a → C) : C

Equations

• Nat.ltGeByCases h₁ h₂ = Decidable.byCases h₁ fun (h : ¬a < b) => h₂ ⋯

@[deprecated ltByCases]

def Nat.ltByCases {a b : Nat} {C : Sort u_2} (h₁ : a < b → C) (h₂ : a = b → C) (h₃ : b < a → C) : C

Equations

• Nat.ltByCases h₁ h₂ h₃ = Nat.ltGeByCases h₁ fun (h₁ : b ≤ a) => Nat.ltGeByCases h₃ fun (h : a ≤ b) => h₂ ⋯

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

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

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

theorem min_le_left {α : Type u_1} [LinearOrder α] (a b : α) : min a b ≤ a

theorem min_le_right {α : Type u_1} [LinearOrder α] (a b : α) : min a b ≤ b

theorem le_min {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ min a b

theorem le_max_left {α : Type u_1} [LinearOrder α] (a b : α) : a ≤ max a b

theorem le_max_right {α : Type u_1} [LinearOrder α] (a b : α) : b ≤ max a b

theorem max_le {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ c) (h₂ : b ≤ c) : max a b ≤ c

theorem eq_min {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c ≤ a) (h₂ : c ≤ b) (h₃ : ∀ {d : α}, d ≤ a → d ≤ b → d ≤ c) : c = min a b

theorem min_comm {α : Type u_1} [LinearOrder α] (a b : α) : min a b = min b a

theorem min_assoc {α : Type u_1} [LinearOrder α] (a b c : α) : min (min a b) c = min a (min b c)

theorem min_left_comm {α : Type u_1} [LinearOrder α] (a b c : α) : min a (min b c) = min b (min a c)

@[simp]

theorem min_self {α : Type u_1} [LinearOrder α] (a : α) : min a a = a

theorem min_eq_left {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : min a b = a

theorem min_eq_right {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) : min a b = b

theorem eq_max {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ c) (h₂ : b ≤ c) (h₃ : ∀ {d : α}, a ≤ d → b ≤ d → c ≤ d) : c = max a b

theorem max_comm {α : Type u_1} [LinearOrder α] (a b : α) : max a b = max b a

theorem max_assoc {α : Type u_1} [LinearOrder α] (a b c : α) : max (max a b) c = max a (max b c)

theorem max_left_comm {α : Type u_1} [LinearOrder α] (a b c : α) : max a (max b c) = max b (max a c)

@[simp]

theorem max_self {α : Type u_1} [LinearOrder α] (a : α) : max a a = a

theorem max_eq_left {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) : max a b = a

theorem max_eq_right {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : max a b = b

theorem min_eq_left_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : min a b = a

theorem min_eq_right_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : b < a) : min a b = b

theorem max_eq_left_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : b < a) : max a b = a

theorem max_eq_right_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : max a b = b

theorem lt_min {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a < b) (h₂ : a < c) : a < min b c

theorem max_lt {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a < c) (h₂ : b < c) : max a b < c

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

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

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

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

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

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

theorem cmp_eq_compare {α : Type u_1} [LinearOrder α] (a b : α) : cmp a b = compare a b

theorem cmp_eq_compareOfLessAndEq {α : Type u_1} [LinearOrder α] (a b : α) : cmp a b = compareOfLessAndEq a b

theorem instLawfulCmpCompare_mathlib {α : Type u_1} [LinearOrder α] : Batteries.LawfulCmp compare