# 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.
def cmpLE {α : Type u_3} [LE α] [DecidableRel fun (x x_1 : α) => x x_1] (x : α) (y : α) :

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

Equations
Instances For
theorem cmpLE_swap {α : Type u_3} [LE α] [IsTotal α fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : α) => x x_1] (x : α) (y : α) :
(cmpLE x y).swap = cmpLE y x
theorem cmpLE_eq_cmp {α : Type u_3} [] [IsTotal α fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : α) => x < x_1] (x : α) (y : α) :
cmpLE x y = cmp x y
def Ordering.Compares {α : Type u_1} [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
Instances For
@[simp]
theorem Ordering.compares_lt {α : Type u_1} [LT α] (a : α) (b : α) :
Ordering.lt.Compares a b = (a < b)
@[simp]
theorem Ordering.compares_eq {α : Type u_1} [LT α] (a : α) (b : α) :
Ordering.eq.Compares a b = (a = b)
@[simp]
theorem Ordering.compares_gt {α : Type u_1} [LT α] (a : α) (b : α) :
Ordering.gt.Compares a b = (a > b)
theorem Ordering.compares_swap {α : Type u_1} [LT α] {a : α} {b : α} {o : Ordering} :
o.swap.Compares a b o.Compares b a
theorem Ordering.Compares.swap {α : Type u_1} [LT α] {a : α} {b : α} {o : Ordering} :
o.Compares b ao.swap.Compares a b

Alias of the reverse direction of Ordering.compares_swap.

theorem Ordering.Compares.of_swap {α : Type u_1} [LT α] {a : α} {b : α} {o : Ordering} :
o.swap.Compares a bo.Compares b a

Alias of the forward direction of Ordering.compares_swap.

theorem Ordering.swap_eq_iff_eq_swap {o : Ordering} {o' : Ordering} :
o.swap = o' o = o'.swap
theorem Ordering.Compares.eq_lt {α : Type u_1} [] {o : Ordering} {a : α} {b : α} :
o.Compares a b( a < b)
theorem Ordering.Compares.ne_lt {α : Type u_1} [] {o : Ordering} {a : α} {b : α} :
o.Compares a b( b a)
theorem Ordering.Compares.eq_eq {α : Type u_1} [] {o : Ordering} {a : α} {b : α} :
o.Compares a b( a = b)
theorem Ordering.Compares.eq_gt {α : Type u_1} [] {o : Ordering} {a : α} {b : α} (h : o.Compares a b) :
b < a
theorem Ordering.Compares.ne_gt {α : Type u_1} [] {o : Ordering} {a : α} {b : α} (h : o.Compares a b) :
a b
theorem Ordering.Compares.le_total {α : Type u_1} [] {a : α} {b : α} {o : Ordering} :
o.Compares a ba b b a
theorem Ordering.Compares.le_antisymm {α : Type u_1} [] {a : α} {b : α} {o : Ordering} :
o.Compares a ba bb aa = b
theorem Ordering.Compares.inj {α : Type u_1} [] {o₁ : Ordering} {o₂ : Ordering} {a : α} {b : α} :
o₁.Compares a bo₂.Compares a bo₁ = o₂
theorem Ordering.compares_iff_of_compares_impl {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} {a' : β} {b' : β} (h : ∀ {o : Ordering}, o.Compares a bo.Compares a' b') (o : Ordering) :
o.Compares a b o.Compares a' b'
theorem Ordering.swap_orElse (o₁ : Ordering) (o₂ : Ordering) :
(o₁.orElse o₂).swap = o₁.swap.orElse o₂.swap
theorem Ordering.orElse_eq_lt (o₁ : Ordering) (o₂ : Ordering) :
o₁.orElse o₂ = Ordering.lt
@[simp]
theorem toDual_compares_toDual {α : Type u_1} [LT α] {a : α} {b : α} {o : Ordering} :
o.Compares (OrderDual.toDual a) (OrderDual.toDual b) o.Compares b a
@[simp]
theorem ofDual_compares_ofDual {α : Type u_1} [LT α] {a : αᵒᵈ} {b : αᵒᵈ} {o : Ordering} :
o.Compares (OrderDual.ofDual a) (OrderDual.ofDual b) o.Compares b a
theorem cmp_compares {α : Type u_1} [] (a : α) (b : α) :
(cmp a b).Compares a b
theorem Ordering.Compares.cmp_eq {α : Type u_1} [] {a : α} {b : α} {o : Ordering} (h : o.Compares a b) :
cmp a b = o
@[simp]
theorem cmp_swap {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x < x_1] (a : α) (b : α) :
(cmp a b).swap = cmp b a
@[simp]
theorem cmpLE_toDual {α : Type u_1} [LE α] [DecidableRel fun (x x_1 : α) => x x_1] (x : α) (y : α) :
cmpLE (OrderDual.toDual x) (OrderDual.toDual y) = cmpLE y x
@[simp]
theorem cmpLE_ofDual {α : Type u_1} [LE α] [DecidableRel fun (x x_1 : α) => x x_1] (x : αᵒᵈ) (y : αᵒᵈ) :
cmpLE (OrderDual.ofDual x) (OrderDual.ofDual y) = cmpLE y x
@[simp]
theorem cmp_toDual {α : Type u_1} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] (x : α) (y : α) :
cmp (OrderDual.toDual x) (OrderDual.toDual y) = cmp y x
@[simp]
theorem cmp_ofDual {α : Type u_1} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] (x : αᵒᵈ) (y : αᵒᵈ) :
cmp (OrderDual.ofDual x) (OrderDual.ofDual y) = cmp y x
def linearOrderOfCompares {α : Type u_1} [] (cmp : ααOrdering) (h : ∀ (a b : α), (cmp a b).Compares a b) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem cmp_eq_lt_iff {α : Type u_1} [] (x : α) (y : α) :
@[simp]
theorem cmp_eq_eq_iff {α : Type u_1} [] (x : α) (y : α) :
@[simp]
theorem cmp_eq_gt_iff {α : Type u_1} [] (x : α) (y : α) :
@[simp]
theorem cmp_self_eq_eq {α : Type u_1} [] (x : α) :
theorem cmp_eq_cmp_symm {α : Type u_1} [] {x : α} {y : α} {β : Type u_3} [] {x' : β} {y' : β} :
cmp x y = cmp x' y' cmp y x = cmp y' x'
theorem lt_iff_lt_of_cmp_eq_cmp {α : Type u_1} [] {x : α} {y : α} {β : Type u_3} [] {x' : β} {y' : β} (h : cmp x y = cmp x' y') :
x < y x' < y'
theorem le_iff_le_of_cmp_eq_cmp {α : Type u_1} [] {x : α} {y : α} {β : Type u_3} [] {x' : β} {y' : β} (h : cmp x y = cmp x' y') :
x y x' y'
theorem eq_iff_eq_of_cmp_eq_cmp {α : Type u_1} [] {x : α} {y : α} {β : Type u_3} [] {x' : β} {y' : β} (h : cmp x y = cmp x' y') :
x = y x' = y'
theorem LT.lt.cmp_eq_lt {α : Type u_1} [] {x : α} {y : α} (h : x < y) :
theorem LT.lt.cmp_eq_gt {α : Type u_1} [] {x : α} {y : α} (h : x < y) :
theorem Eq.cmp_eq_eq {α : Type u_1} [] {x : α} {y : α} (h : x = y) :
theorem Eq.cmp_eq_eq' {α : Type u_1} [] {x : α} {y : α} (h : x = y) :