Documentation

Std.Classes.Order

Ordering #

@[simp]
theorem Ordering.swap_inj {o₁ : Ordering} {o₂ : Ordering} :
Ordering.swap o₁ = Ordering.swap o₂ o₁ = o₂
class Std.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
    class Std.OrientedCmp {α : Sort u_1} (cmp : ααOrdering) :

    OrientedCmp cmp asserts that cmp is determined by the relation cmp x y = .lt.

    • symm : ∀ (x y : α), Ordering.swap (cmp x y) = cmp y x

      The comparator operation is symmetric, in the sense that if cmp x y equals .lt then cmp y x = .gt and vice versa.

    Instances
      theorem Std.OrientedCmp.cmp_eq_gt :
      ∀ {α : Sort u_1} {cmp : ααOrdering} {x y : α} [inst : Std.OrientedCmp cmp], cmp x y = Ordering.gt cmp y x = Ordering.lt
      theorem Std.OrientedCmp.cmp_eq_eq_symm :
      ∀ {α : Sort u_1} {cmp : ααOrdering} {x y : α} [inst : Std.OrientedCmp cmp], cmp x y = Ordering.eq cmp y x = Ordering.eq
      theorem Std.OrientedCmp.cmp_refl :
      ∀ {α : Sort u_1} {cmp : ααOrdering} {x : α} [inst : Std.OrientedCmp cmp], cmp x x = Ordering.eq
      class Std.TransCmp {α : Sort u_1} (cmp : ααOrdering) extends Std.OrientedCmp :

      TransCmp cmp asserts that cmp induces a transitive relation.

      Instances
        theorem Std.TransCmp.ge_trans :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y Ordering.ltcmp y z Ordering.ltcmp x_1 z Ordering.lt
        theorem Std.TransCmp.lt_asymm :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Std.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.ltcmp y x_1 Ordering.lt
        theorem Std.TransCmp.gt_asymm :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Std.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.gtcmp y x_1 Ordering.gt
        theorem Std.TransCmp.le_lt_trans :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y Ordering.gtcmp y z = Ordering.ltcmp x_1 z = Ordering.lt
        theorem Std.TransCmp.lt_le_trans :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.ltcmp y z Ordering.gtcmp x_1 z = Ordering.lt
        theorem Std.TransCmp.lt_trans :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.ltcmp y z = Ordering.ltcmp x_1 z = Ordering.lt
        theorem Std.TransCmp.gt_trans :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.gtcmp y z = Ordering.gtcmp x_1 z = Ordering.gt
        theorem Std.TransCmp.cmp_congr_left :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.eqcmp x_1 z = cmp y z
        theorem Std.TransCmp.cmp_congr_left' :
        ∀ {x : Sort u_1} {cmp : xxOrdering} [inst : Std.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.eqcmp x_1 = cmp y
        theorem Std.TransCmp.cmp_congr_right :
        ∀ {x : Sort u_1} {cmp : xxOrdering} {y z x_1 : x} [inst : Std.TransCmp cmp], cmp y z = Ordering.eqcmp x_1 y = cmp x_1 z
        @[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
          instance Ordering.instOrientedCmpByKey {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) [Std.OrientedCmp cmp] :
          Equations
          • =
          instance Ordering.instTransCmpByKey {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) [Std.TransCmp cmp] :
          Equations
          • =
          instance Ordering.instTransCmpByKey_1 {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) [Std.TransCmp cmp] :
          Equations
          • =