Documentation

Mathlib.Data.Ordering.Basic

Helper definitions and instances for Ordering #

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 : α) :
      lt.Compares a b = (a < b)
      @[simp]
      theorem Ordering.compares_eq {α : Type u_1} [LT α] (a b : α) :
      eq.Compares a b = (a = b)
      @[simp]
      theorem Ordering.compares_gt {α : Type u_1} [LT α] (a b : α) :
      gt.Compares a b = (a > b)
      @[macro_inline]
      def Ordering.dthen (o : Ordering) :
      (o = eqOrdering)Ordering

      o₁.dthen fun h => o₂(h) is like o₁.then o₂ but o₂ is allowed to depend on h : o₁ = .eq.

      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 α] [DecidableLT α] (a b : α) :

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

              Equations
                Instances For