order.compare

# Comparison #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Definitions #

• cmp_le: An ordering from ≤.
• ordering.compares: Turns an ordering into < and = propositions.
• linear_order_of_compares: Constructs a linear_order instance from the fact that any two elements that are not one strictly less than the other either way are equal.
def cmp_le {α : Type u_1} [has_le α] (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
theorem cmp_le_swap {α : Type u_1} [has_le α] (x y : α) :
(cmp_le x y).swap = x
theorem cmp_le_eq_cmp {α : Type u_1} [preorder α] (x y : α) :
y = cmp x y
@[simp]
def ordering.compares {α : Type u_1} [has_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
• = (a > b)
• = (a = b)
• = (a < b)
theorem ordering.compares_swap {α : Type u_1} [has_lt α] {a b : α} {o : ordering} :
theorem ordering.compares.of_swap {α : Type u_1} [has_lt α] {a b : α} {o : ordering} :

Alias of the forward direction of ordering.compares_swap.

theorem ordering.compares.swap {α : Type u_1} [has_lt α] {a b : α} {o : ordering} :

Alias of the reverse direction of ordering.compares_swap.

@[simp]
theorem ordering.swap_inj (o₁ o₂ : ordering) :
o₁.swap = o₂.swap o₁ = o₂
theorem ordering.swap_eq_iff_eq_swap {o o' : ordering} :
o.swap = o' o = o'.swap
theorem ordering.compares.eq_lt {α : Type u_1} [preorder α] {o : ordering} {a b : α} :
o.compares a b a < b)
theorem ordering.compares.ne_lt {α : Type u_1} [preorder α] {o : ordering} {a b : α} :
o.compares a b b a)
theorem ordering.compares.eq_eq {α : Type u_1} [preorder α] {o : ordering} {a b : α} :
o.compares a b a = b)
theorem ordering.compares.eq_gt {α : Type u_1} [preorder α] {o : ordering} {a b : α} (h : o.compares a b) :
b < a
theorem ordering.compares.ne_gt {α : Type u_1} [preorder α] {o : ordering} {a b : α} (h : o.compares a b) :
a b
theorem ordering.compares.le_total {α : Type u_1} [preorder α] {a b : α} {o : ordering} :
o.compares a b a b b a
theorem ordering.compares.le_antisymm {α : Type u_1} [preorder α] {a b : α} {o : ordering} :
o.compares a b a b b a a = b
theorem ordering.compares.inj {α : Type u_1} [preorder α] {o₁ o₂ : ordering} {a b : α} :
o₁.compares a b o₂.compares a b o₁ = o₂
theorem ordering.compares_iff_of_compares_impl {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a b : α} {a' b' : β} (h : {o : ordering}, o.compares a b o.compares a' b') (o : ordering) :
o.compares a b o.compares a' b'
theorem ordering.swap_or_else (o₁ o₂ : ordering) :
(o₁.or_else o₂).swap = o₁.swap.or_else o₂.swap
theorem ordering.or_else_eq_lt (o₁ o₂ : ordering) :
@[simp]
theorem to_dual_compares_to_dual {α : Type u_1} [has_lt α] {a b : α} {o : ordering} :
o.compares b a
@[simp]
theorem of_dual_compares_of_dual {α : Type u_1} [has_lt α] {a b : αᵒᵈ} {o : ordering} :
o.compares b a
theorem cmp_compares {α : Type u_1} [linear_order α] (a b : α) :
(cmp a b).compares a b
theorem ordering.compares.cmp_eq {α : Type u_1} [linear_order α] {a b : α} {o : ordering} (h : o.compares a b) :
cmp a b = o
@[simp]
theorem cmp_swap {α : Type u_1} [preorder α] (a b : α) :
(cmp a b).swap = cmp b a
@[simp]
theorem cmp_le_to_dual {α : Type u_1} [has_le α] (x y : α) :
= x
@[simp]
theorem cmp_le_of_dual {α : Type u_1} [has_le α] (x y : αᵒᵈ) :
= x
@[simp]
theorem cmp_to_dual {α : Type u_1} [has_lt α] (x y : α) :
= cmp y x
@[simp]
theorem cmp_of_dual {α : Type u_1} [has_lt α] (x y : αᵒᵈ) :
= cmp y x
def linear_order_of_compares {α : Type u_1} [preorder α] (cmp : α ) (h : (a b : α), (cmp a b).compares a b) :

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

Equations
@[simp]
theorem cmp_eq_lt_iff {α : Type u_1} [linear_order α] (x y : α) :
@[simp]
theorem cmp_eq_eq_iff {α : Type u_1} [linear_order α] (x y : α) :
@[simp]
theorem cmp_eq_gt_iff {α : Type u_1} [linear_order α] (x y : α) :
@[simp]
theorem cmp_self_eq_eq {α : Type u_1} [linear_order α] (x : α) :
theorem cmp_eq_cmp_symm {α : Type u_1} [linear_order α] {x y : α} {β : Type u_2} [linear_order β] {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} [linear_order α] {x y : α} {β : Type u_2} [linear_order β] {x' y' : β} (h : cmp x y = cmp x' y') :
x < y x' < y'
theorem le_iff_le_of_cmp_eq_cmp {α : Type u_1} [linear_order α] {x y : α} {β : Type u_2} [linear_order β] {x' y' : β} (h : cmp x y = cmp x' y') :
x y x' y'
theorem eq_iff_eq_of_cmp_eq_cmp {α : Type u_1} [linear_order α] {x y : α} {β : Type u_2} [linear_order β] {x' y' : β} (h : cmp x y = cmp x' y') :
x = y x' = y'
theorem has_lt.lt.cmp_eq_lt {α : Type u_1} [linear_order α] {x y : α} (h : x < y) :
theorem has_lt.lt.cmp_eq_gt {α : Type u_1} [linear_order α] {x y : α} (h : x < y) :
theorem eq.cmp_eq_eq {α : Type u_1} [linear_order α] {x y : α} (h : x = y) :
theorem eq.cmp_eq_eq' {α : Type u_1} [linear_order α] {x y : α} (h : x = y) :