Documentation

Batteries.Classes.Order

theorem lexOrd_def {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
compare = compareLex (compareOn fun (x : α × β) => x.fst) (compareOn fun (x : α × β) => x.snd)
@[inline]
def Ordering.byKey {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) (a b : α) :

Pull back a comparator by a function f, by applying the comparator to both arguments.

Equations
Instances For
    class Batteries.TotalBLE {α : Sort u_1} (le : ααBool) :

    TotalBLE le asserts that le has a total order, that is, le a b ∨ le b a.

    • total {a b : α} : le a b = true le b a = true

      le is total: either le a b or le b a.

    Instances

      Batteries features not in core Std

      theorem Std.OrientedCmp.le_iff_ge {α : Type u_1} {cmp : ααOrdering} [OrientedCmp cmp] {x y : α} :
      theorem Std.TransCmp.le_trans {α : Type u_1} {cmp : ααOrdering} [TransCmp cmp] {x y z : α} :
      cmp x y Ordering.gtcmp y z Ordering.gtcmp x z Ordering.gt
      theorem Std.TransCmp.lt_of_lt_of_le {α : Type u_1} {cmp : ααOrdering} [TransCmp cmp] {x y z : α} :
      cmp x y = Ordering.ltcmp y z Ordering.gtcmp x z = Ordering.lt
      theorem Std.TransCmp.lt_of_le_of_lt {α : Type u_1} {cmp : ααOrdering} [TransCmp cmp] {x y z : α} :
      cmp x y Ordering.gtcmp y z = Ordering.ltcmp x z = Ordering.lt
      theorem Std.TransCmp.ge_trans {α : Type u_1} {cmp : ααOrdering} [TransCmp cmp] {x y z : α} :
      cmp x y Ordering.ltcmp y z Ordering.ltcmp x z Ordering.lt
      theorem Std.TransCmp.gt_of_gt_of_ge {α : Type u_1} {cmp : ααOrdering} [TransCmp cmp] {x y z : α} :
      cmp x y = Ordering.gtcmp y z Ordering.ltcmp x z = Ordering.gt
      theorem Std.TransCmp.gt_of_ge_of_gt {α : Type u_1} {cmp : ααOrdering} [TransCmp cmp] {x y z : α} :
      cmp x y Ordering.ltcmp y z = Ordering.gtcmp x z = Ordering.gt
      class Std.LawfulLTCmp {α : Type u_1} [LT α] (cmp : ααOrdering) extends Std.OrientedCmp cmp :

      LawfulLTCmp cmp asserts that cmp x y = .lt and x < y coincide.

      • eq_swap {a b : α} : cmp a b = (cmp b a).swap
      • eq_lt_iff_lt {x y : α} : cmp x y = Ordering.lt x < y

        cmp x y = .lt holds iff x < y is true.

      Instances
        theorem Std.LawfulLTCmp.eq_gt_iff_gt {α : Type u_1} {cmp : ααOrdering} {x y : α} [LT α] [LawfulLTCmp cmp] :
        cmp x y = Ordering.gt y < x
        class Std.LawfulLECmp {α : Type u_1} [LE α] (cmp : ααOrdering) extends Std.OrientedCmp cmp :

        LawfulLECmp cmp asserts that (cmp x y).isLE and x ≤ y coincide.

        • eq_swap {a b : α} : cmp a b = (cmp b a).swap
        • isLE_iff_le {x y : α} : (cmp x y).isLE = true x y

          cmp x y ≠ .gt holds iff x ≤ y is true.

        Instances
          theorem Std.LawfulLECmp.isGE_iff_ge {α : Type u_1} {cmp : ααOrdering} {x y : α} [LE α] [LawfulLECmp cmp] :
          (cmp x y).isGE = true y x
          theorem Std.LawfulLECmp.ne_gt_iff_le {α : Type u_1} {cmp : ααOrdering} {x y : α} [LE α] [LawfulLECmp cmp] :
          cmp x y Ordering.gt x y
          theorem Std.LawfulLECmp.ne_lt_iff_ge {α : Type u_1} {cmp : ααOrdering} {x y : α} [LE α] [LawfulLECmp cmp] :
          cmp x y Ordering.lt y x
          class Std.LawfulBCmp {α : Type u_1} [LE α] [LT α] [BEq α] (cmp : ααOrdering) extends Std.TransCmp cmp, Std.LawfulBEqCmp cmp, Std.LawfulLTCmp cmp, Std.LawfulLECmp cmp :

          LawfulBCmp cmp asserts that the LE, LT, BEq are all coherent with each other and with cmp, describing a strict weak order (a linear order except for antisymmetry).

          Instances
            class Std.LawfulCmp {α : Type u_1} [LE α] [LT α] (cmp : ααOrdering) extends Std.TransCmp cmp, Std.LawfulEqCmp cmp, Std.LawfulLTCmp cmp, Std.LawfulLECmp cmp :

            LawfulBCmp cmp asserts that the LE, LT, Eq are all coherent with each other and with cmp, describing a linear order.

            Instances
              @[reducible, inline]
              abbrev Std.LawfulLTOrd (α : Type u_1) [LT α] [Ord α] :

              Class for types where the ordering function is compatible with the LT.

              Equations
              Instances For
                @[reducible, inline]
                abbrev Std.LawfulLEOrd (α : Type u_1) [LE α] [Ord α] :

                Class for types where the ordering function is compatible with the LE.

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev Std.LawfulBOrd (α : Type u_1) [LE α] [LT α] [BEq α] [Ord α] :

                  Class for types where the ordering function is compatible with the LE, LT and BEq.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev Std.LawfulOrd (α : Type u_1) [LE α] [LT α] [Ord α] :

                    Class for types where the ordering function is compatible with the LE, LT and Eq.

                    Equations
                    Instances For
                      instance Std.instOrientedCmpFlipOrdering_batteries {α✝ : Type u_1} {cmp : α✝α✝Ordering} [inst : OrientedCmp cmp] :
                      instance Std.instTransCmpFlipOrdering_batteries {α✝ : Type u_1} {cmp : α✝α✝Ordering} [inst : TransCmp cmp] :
                      instance Std.instOrientedCmpByKey {α : Type u_1} {β : Type u_2} (f : αβ) (cmp : ββOrdering) [OrientedCmp cmp] :
                      instance Std.instTransCmpByKey {α : Type u_1} {β : Type u_2} (f : αβ) (cmp : ββOrdering) [TransCmp cmp] :
                      instance Std.instOrientedCmpCompareLex_batteries {α✝ : Type u_1} {cmp₁ cmp₂ : α✝α✝Ordering} [inst₁ : OrientedCmp cmp₁] [inst₂ : OrientedCmp cmp₂] :
                      OrientedCmp (compareLex cmp₁ cmp₂)
                      instance Std.instTransCmpCompareLex_batteries {α✝ : Type u_1} {cmp₁ cmp₂ : α✝α✝Ordering} [inst₁ : TransCmp cmp₁] [inst₂ : TransCmp cmp₂] :
                      TransCmp (compareLex cmp₁ cmp₂)
                      instance Std.instOrientedCmpCompareOnOfOrientedOrd_batteries {β : Type u_1} {α : Type u_2} [Ord β] [OrientedOrd β] (f : αβ) :
                      instance Std.instTransCmpCompareOnOfTransOrd_batteries {β : Type u_1} {α : Type u_2} [Ord β] [TransOrd β] (f : αβ) :
                      theorem Std.OrientedOrd.instOn {β : Type u_1} {α : Type u_2} [ord : Ord β] [OrientedOrd β] (f : αβ) :
                      theorem Std.TransOrd.instOn {β : Type u_1} {α : Type u_2} [ord : Ord β] [TransOrd β] (f : αβ) :
                      theorem Std.OrientedOrd.instOrdLex' {α : Type u_1} (ord₁ ord₂ : Ord α) [OrientedOrd α] [OrientedOrd α] :
                      theorem Std.TransOrd.instOrdLex' {α : Type u_1} (ord₁ ord₂ : Ord α) [TransOrd α] [TransOrd α] :
                      theorem Std.LawfulLTCmp.eq_compareOfLessAndEq {α : Type u_1} {cmp : ααOrdering} [LT α] [DecidableEq α] [LawfulEqCmp cmp] [LawfulLTCmp cmp] (x y : α) [Decidable (x < y)] :
                      cmp x y = compareOfLessAndEq x y
                      theorem Std.ReflCmp.compareOfLessAndEq_of_lt_irrefl {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] (lt_irrefl : ∀ (x : α), ¬x < x) :
                      ReflCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
                      theorem Std.LawfulBEqCmp.compareOfLessAndEq_of_lt_irrefl {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] [BEq α] [LawfulBEq α] (lt_irrefl : ∀ (x : α), ¬x < x) :
                      LawfulBEqCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
                      theorem Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (lt_antisymm : ∀ {x y : α}, ¬x < y¬y < xx = y) :
                      TransCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
                      theorem Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm {α : Type u_1} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < yy x) (le_antisymm : ∀ {x y : α}, x yy xx = y) :
                      TransCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
                      theorem Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (lt_antisymm : ∀ {x y : α}, ¬x < y¬y < xx = y) :
                      LawfulLTCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
                      theorem Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] [LE α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < yy x) (le_antisymm : ∀ {x y : α}, x yy xx = y) :
                      LawfulLTCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
                      theorem Std.LawfulLECmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] [LE α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < y y x) (le_antisymm : ∀ {x y : α}, x yy xx = y) :
                      LawfulLECmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
                      theorem Std.LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm {α : Type u_1} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α] (lt_irrefl : ∀ (x : α), ¬x < x) (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (not_lt : ∀ {x y : α}, ¬x < y y x) (le_antisymm : ∀ {x y : α}, x yy xx = y) :
                      LawfulCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2