Ordering

@[simp]

theorem Ordering.swap_swap {o : Ordering} : Ordering.swap (Ordering.swap o) = o

@[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) : Prop

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

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

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

class Std.OrientedCmp {α : Sort u_1} (cmp : α → α → Ordering) : Prop

• 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.

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

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 : Prop

• symm : ∀ (x y : α), Ordering.swap (cmp x y) = cmp y x
• le_trans : ∀ {x y z : α}, cmp x y ≠ Ordering.gt → cmp y z ≠ Ordering.gt → cmp x z ≠ Ordering.gt

  The comparator operation is transitive.

TransCmp cmp asserts that cmp induces a transitive relation.

theorem Std.TransCmp.ge_trans : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y ≠ Ordering.lt → cmp y z ≠ Ordering.lt → cmp x_1 z ≠ Ordering.lt

theorem Std.TransCmp.lt_asymm : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Std.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.lt → cmp y x_1 ≠ Ordering.lt

theorem Std.TransCmp.gt_asymm : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Std.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.gt → cmp y x_1 ≠ Ordering.gt

theorem Std.TransCmp.le_lt_trans : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y ≠ Ordering.gt → cmp y z = Ordering.lt → cmp x_1 z = Ordering.lt

theorem Std.TransCmp.lt_le_trans : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.lt → cmp y z ≠ Ordering.gt → cmp x_1 z = Ordering.lt

theorem Std.TransCmp.lt_trans : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.lt → cmp y z = Ordering.lt → cmp x_1 z = Ordering.lt

theorem Std.TransCmp.gt_trans : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.gt → cmp y z = Ordering.gt → cmp x_1 z = Ordering.gt

theorem Std.TransCmp.cmp_congr_left : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Std.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.eq → cmp x_1 z = cmp y z

theorem Std.TransCmp.cmp_congr_left' : ∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Std.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.eq → cmp x_1 = cmp y

theorem Std.TransCmp.cmp_congr_right : ∀ {x : Sort u_1} {cmp : x → x → Ordering} {y z x_1 : x} [inst : Std.TransCmp cmp], cmp y z = Ordering.eq → cmp x_1 y = cmp x_1 z

@[inline]

def Std.byKey {α : Sort u_1} {β : Sort u_2} (f : α → β) (cmp : β → β → Ordering) (a : α) (b : α) : Ordering

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

Equations

• Std.byKey f cmp a b = cmp (f a) (f b)

instance Std.instOrientedCmpByKey {α : Sort u_1} {β : Sort u_2} (f : α → β) (cmp : β → β → Ordering) [Std.OrientedCmp cmp] : Std.OrientedCmp (Std.byKey f cmp)

Equations

• @Std.instOrientedCmpByKey = @Std.instOrientedCmpByKey.proof_1

instance Std.instTransCmpByKey {α : Sort u_1} {β : Sort u_2} (f : α → β) (cmp : β → β → Ordering) [Std.TransCmp cmp] : Std.TransCmp (Std.byKey f cmp)

Equations

• @Std.instTransCmpByKey = @Std.instTransCmpByKey.proof_1

instance Std.instTransCmpByKey_1 {α : Sort u_1} {β : Sort u_2} (f : α → β) (cmp : β → β → Ordering) [Std.TransCmp cmp] : Std.TransCmp (Std.byKey f cmp)

Equations

• @Std.instTransCmpByKey_1 = @Std.instTransCmpByKey_1.proof_1