# Documentation

Std.Classes.Order

## Ordering #

@[simp]
@[simp]
theorem Ordering.swap_inj {o₁ : Ordering} {o₂ : Ordering} :
o₁ = o₂
class Std.TotalBLE {α : Sort u_1} (le : ααBool) :
• le is total: either le a b or le b a.

total : ∀ {a b : α}, le a b = true le b a = true

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

Instances
class Std.OrientedCmp {α : Sort u_1} (cmp : ααOrdering) :
• The comparator operation is symmetric, in the sense that if cmp x y equals .lt then cmp y x = .gt and vice versa.

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

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

Instances
theorem Std.OrientedCmp.cmp_eq_gt :
∀ {α : Sort u_1} {cmp : ααOrdering} {x y : α} [inst : ], 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 : ], cmp x y = Ordering.eq cmp y x = Ordering.eq
theorem Std.OrientedCmp.cmp_refl :
∀ {α : Sort u_1} {cmp : ααOrdering} {x : α} [inst : ], cmp x x = Ordering.eq
class Std.TransCmp {α : Sort u_1} (cmp : ααOrdering) extends :

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_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 Std.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
instance Std.instOrientedCmpByKey {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) [inst : ] :
Equations
instance Std.instTransCmpByKey {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) [inst : Std.TransCmp cmp] :
Equations
instance Std.instTransCmpByKey_1 {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) [inst : Std.TransCmp cmp] :
Equations