Documentation

Mathlib.Data.Ordering.Basic

Helper definitions and instances for Ordering #

@[inline]

Combine two Orderings lexicographically.

Equations
Instances For
    def Ordering.toRel {α : Type u} [LT α] :
    OrderingααProp

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

    Equations
    Instances For
      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
      Instances For
        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
        Instances For