Documentation

Mathlib.Data.Ordering.Basic

Helper definitions and instances for Ordering #

@[deprecated Ordering.then]

Alias of Ordering.then.


If o₁ and o₂ are Ordering, then o₁.then o₂ returns o₁ unless it is .eq, in which case it returns o₂. Additionally, it has "short-circuiting" semantics similar to boolean x && y: if o₁ is not .eq then the expression for o₂ is not evaluated. This is a useful primitive for constructing lexicographic comparator functions:

structure Person where
  name : String
  age : Nat

instance : Ord Person where
  compare a b := (compare a.name b.name).then (compare b.age a.age)

This example will sort people first by name (in ascending order) and will sort people with the same name by age (in descending order). (If all fields are sorted ascending and in the same order as they are listed in the structure, you can also use deriving Ord on the structure definition for the same effect.)

Equations
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
@[deprecated Ordering.Compares]
def Ordering.toRel {α : Type u_1} [LT α] :
OrderingααProp

Alias of Ordering.Compares.


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
@[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)
def cmpUsing {α : Type u} (lt : ααProp) [DecidableRel lt] (a b : α) :

Lift a decidable relation to an Ordering, assuming that incomparable terms are Ordering.eq.

Equations
def cmp {α : Type u} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (a b : α) :

Construct an Ordering from a type with a decidable LT instance, assuming that incomparable terms are Ordering.eq.

Equations