Comparison

This file provides basic results about orderings and comparison in linear orders.

Definitions

• CmpLE: An Ordering from ≤≤.
• Ordering.Compares: Turns an Ordering into < and = propositions.
• linearOrderOfCompares: Constructs a LinearOrder instance from the fact that any two elements that are not one strictly less than the other either way are equal.

ink

def cmpLE {α : Type u_1} [inst : LE α] [inst : DecidableRel fun x x_1 => x ≤ x_1] (x : α) (y : α) : Ordering

Like cmp, but uses a ≤≤ on the type instead of <. Given two elements x and y, returns a three-way comparison result Ordering.

Equations

• cmpLE x y = if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt

ink

theorem cmpLE_swap {α : Type u_1} [inst : LE α] [inst : IsTotal α fun x x_1 => x ≤ x_1] [inst : DecidableRel fun x x_1 => x ≤ x_1] (x : α) (y : α) : Ordering.swap (cmpLE x y) = cmpLE y x

ink

theorem cmpLE_eq_cmp {α : Type u_1} [inst : Preorder α] [inst : IsTotal α fun x x_1 => x ≤ x_1] [inst : DecidableRel fun x x_1 => x ≤ x_1] [inst : DecidableRel fun x x_1 => x < x_1] (x : α) (y : α) : cmpLE x y = cmp x y

ink

def Ordering.Compares {α : Type u_1} [inst : LT α] : Ordering → α → α → Prop

Compares o a b means that a and b have the ordering relation o between them, assuming that the relation a < b is defined.

Equations

• Ordering.Compares x x x = match x, x, x with | Ordering.lt, a, b => a < b | Ordering.eq, a, b => a = b | Ordering.gt, a, b => a > b

ink

@[simp]

theorem Ordering.compares_lt {α : Type u_1} [inst : LT α] (a : α) (b : α) : Ordering.Compares Ordering.lt a b = (a < b)

ink

@[simp]

theorem Ordering.compares_eq {α : Type u_1} [inst : LT α] (a : α) (b : α) : Ordering.Compares Ordering.eq a b = (a = b)

ink

@[simp]

theorem Ordering.compares_gt {α : Type u_1} [inst : LT α] (a : α) (b : α) : Ordering.Compares Ordering.gt a b = (a > b)

ink

theorem Ordering.compares_swap {α : Type u_1} [inst : LT α] {a : α} {b : α} {o : Ordering} : Ordering.Compares (Ordering.swap o) a b ↔ Ordering.Compares o b a

ink

theorem Ordering.Compares.swap {α : Type u_1} [inst : LT α] {a : α} {b : α} {o : Ordering} : Ordering.Compares o b a → Ordering.Compares (Ordering.swap o) a b

Alias of the reverse direction of Ordering.compares_swap.

ink

theorem Ordering.Compares.of_swap {α : Type u_1} [inst : LT α] {a : α} {b : α} {o : Ordering} : Ordering.Compares (Ordering.swap o) a b → Ordering.Compares o b a

Alias of the forward direction of Ordering.compares_swap.

ink

theorem Ordering.swap_eq_iff_eq_swap {o : Ordering} {o' : Ordering} : Ordering.swap o = o' ↔ o = Ordering.swap o'

ink

theorem Ordering.Compares.eq_lt {α : Type u_1} [inst : Preorder α] {o : Ordering} {a : α} {b : α} : Ordering.Compares o a b → (o = Ordering.lt ↔ a < b)

ink

theorem Ordering.Compares.ne_lt {α : Type u_1} [inst : Preorder α] {o : Ordering} {a : α} {b : α} : Ordering.Compares o a b → (o ≠ Ordering.lt ↔ b ≤ a)

ink

theorem Ordering.Compares.eq_eq {α : Type u_1} [inst : Preorder α] {o : Ordering} {a : α} {b : α} : Ordering.Compares o a b → (o = Ordering.eq ↔ a = b)

ink

theorem Ordering.Compares.eq_gt {α : Type u_1} [inst : Preorder α] {o : Ordering} {a : α} {b : α} (h : Ordering.Compares o a b) : o = Ordering.gt ↔ b < a

ink

theorem Ordering.Compares.ne_gt {α : Type u_1} [inst : Preorder α] {o : Ordering} {a : α} {b : α} (h : Ordering.Compares o a b) : o ≠ Ordering.gt ↔ a ≤ b

ink

theorem Ordering.Compares.le_total {α : Type u_1} [inst : Preorder α] {a : α} {b : α} {o : Ordering} : Ordering.Compares o a b → a ≤ b ∨ b ≤ a

ink

theorem Ordering.Compares.le_antisymm {α : Type u_1} [inst : Preorder α] {a : α} {b : α} {o : Ordering} : Ordering.Compares o a b → a ≤ b → b ≤ a → a = b

ink

theorem Ordering.Compares.inj {α : Type u_1} [inst : Preorder α] {o₁ : Ordering} {o₂ : Ordering} {a : α} {b : α} : Ordering.Compares o₁ a b → Ordering.Compares o₂ a b → o₁ = o₂

ink

theorem Ordering.compares_iff_of_compares_impl {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : Preorder β] {a : α} {b : α} {a' : β} {b' : β} (h : ∀ {o : Ordering}, Ordering.Compares o a b → Ordering.Compares o a' b') (o : Ordering) : Ordering.Compares o a b ↔ Ordering.Compares o a' b'

ink

theorem Ordering.swap_orElse (o₁ : Ordering) (o₂ : Ordering) : Ordering.swap (Ordering.orElse o₁ o₂) = Ordering.orElse (Ordering.swap o₁) (Ordering.swap o₂)

ink

theorem Ordering.orElse_eq_lt (o₁ : Ordering) (o₂ : Ordering) : Ordering.orElse o₁ o₂ = Ordering.lt ↔ o₁ = Ordering.lt ∨ o₁ = Ordering.eq ∧ o₂ = Ordering.lt

ink

@[simp]

theorem toDual_compares_toDual {α : Type u_1} [inst : LT α] {a : α} {b : α} {o : Ordering} : Ordering.Compares o (↑OrderDual.toDual a) (↑OrderDual.toDual b) ↔ Ordering.Compares o b a

ink

@[simp]

theorem ofDual_compares_ofDual {α : Type u_1} [inst : LT α] {a : αᵒᵈ} {b : αᵒᵈ} {o : Ordering} : Ordering.Compares o (↑OrderDual.ofDual a) (↑OrderDual.ofDual b) ↔ Ordering.Compares o b a

ink

theorem cmp_compares {α : Type u_1} [inst : LinearOrder α] (a : α) (b : α) : Ordering.Compares (cmp a b) a b

ink

theorem Ordering.Compares.cmp_eq {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} {o : Ordering} (h : Ordering.Compares o a b) : cmp a b = o

ink

@[simp]

theorem cmp_swap {α : Type u_1} [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] (a : α) (b : α) : Ordering.swap (cmp a b) = cmp b a

ink

@[simp]

theorem cmpLE_toDual {α : Type u_1} [inst : LE α] [inst : DecidableRel fun x x_1 => x ≤ x_1] (x : α) (y : α) : cmpLE (↑OrderDual.toDual x) (↑OrderDual.toDual y) = cmpLE y x

ink

@[simp]

theorem cmpLE_ofDual {α : Type u_1} [inst : LE α] [inst : DecidableRel fun x x_1 => x ≤ x_1] (x : αᵒᵈ) (y : αᵒᵈ) : cmpLE (↑OrderDual.ofDual x) (↑OrderDual.ofDual y) = cmpLE y x

ink

@[simp]

theorem cmp_toDual {α : Type u_1} [inst : LT α] [inst : DecidableRel fun x x_1 => x < x_1] (x : α) (y : α) : cmp (↑OrderDual.toDual x) (↑OrderDual.toDual y) = cmp y x

ink

@[simp]

theorem cmp_ofDual {α : Type u_1} [inst : LT α] [inst : DecidableRel fun x x_1 => x < x_1] (x : αᵒᵈ) (y : αᵒᵈ) : cmp (↑OrderDual.ofDual x) (↑OrderDual.ofDual y) = cmp y x

ink

def linearOrderOfCompares {α : Type u_1} [inst : Preorder α] (cmp : α → α → Ordering) (h : ∀ (a b : α), Ordering.Compares (cmp a b) a b) : LinearOrder α

Generate a linear order structure from a preorder and cmp function.

Equations

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

ink

@[simp]

theorem cmp_eq_lt_iff {α : Type u_1} [inst : LinearOrder α] (x : α) (y : α) : cmp x y = Ordering.lt ↔ x < y

ink

@[simp]

theorem cmp_eq_eq_iff {α : Type u_1} [inst : LinearOrder α] (x : α) (y : α) : cmp x y = Ordering.eq ↔ x = y

ink

@[simp]

theorem cmp_eq_gt_iff {α : Type u_1} [inst : LinearOrder α] (x : α) (y : α) : cmp x y = Ordering.gt ↔ y < x

ink

@[simp]

theorem cmp_self_eq_eq {α : Type u_1} [inst : LinearOrder α] (x : α) : cmp x x = Ordering.eq

ink

theorem cmp_eq_cmp_symm {α : Type u_1} [inst : LinearOrder α] {x : α} {y : α} {β : Type u_2} [inst : LinearOrder β] {x' : β} {y' : β} : cmp x y = cmp x' y' ↔ cmp y x = cmp y' x'

ink

theorem lt_iff_lt_of_cmp_eq_cmp {α : Type u_1} [inst : LinearOrder α] {x : α} {y : α} {β : Type u_2} [inst : LinearOrder β] {x' : β} {y' : β} (h : cmp x y = cmp x' y') : x < y ↔ x' < y'

ink

theorem le_iff_le_of_cmp_eq_cmp {α : Type u_1} [inst : LinearOrder α] {x : α} {y : α} {β : Type u_2} [inst : LinearOrder β] {x' : β} {y' : β} (h : cmp x y = cmp x' y') : x ≤ y ↔ x' ≤ y'

ink

theorem eq_iff_eq_of_cmp_eq_cmp {α : Type u_1} [inst : LinearOrder α] {x : α} {y : α} {β : Type u_2} [inst : LinearOrder β] {x' : β} {y' : β} (h : cmp x y = cmp x' y') : x = y ↔ x' = y'

ink

theorem LT.lt.cmp_eq_lt {α : Type u_1} [inst : LinearOrder α] {x : α} {y : α} (h : x < y) : cmp x y = Ordering.lt

ink

theorem LT.lt.cmp_eq_gt {α : Type u_1} [inst : LinearOrder α] {x : α} {y : α} (h : x < y) : cmp y x = Ordering.gt

ink

theorem Eq.cmp_eq_eq {α : Type u_1} [inst : LinearOrder α] {x : α} {y : α} (h : x = y) : cmp x y = Ordering.eq

ink

theorem Eq.cmp_eq_eq' {α : Type u_1} [inst : LinearOrder α] {x : α} {y : α} (h : x = y) : cmp y x = Ordering.eq