Documentation

Mathlib.Init.Data.Ordering.Basic

Helper definitions and instances for Ordering #

@[inline]

Combine two Orderings lexicographically.

Equations
def Ordering.toRel {α : Type u_1} [inst : LT α] :
OrderingααProp

The relation corresponding to each Ordering constructor (e.g. .lt.toProp a b is a < b).

Equations
def cmpUsing {α : Type u} (lt : ααProp) [inst : DecidableRel lt] (a : α) (b : α) :

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

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

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

Equations