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 : α) : Ordering

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

Equations

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

class Batteries.TotalBLE {α : Sort u_1} (le : α → α → Bool) : Prop

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.

theorem Batteries.compareOfLessAndEq_eq_lt {α : Type u_1} {x y : α} [LT α] [Decidable (x < y)] [DecidableEq α] : compareOfLessAndEq x y = Ordering.lt ↔ x < y

Batteries features not in core Std

theorem Std.OrientedCmp.le_iff_ge {α : Type u_1} {cmp : α → α → Ordering} [OrientedCmp cmp] {x y : α} : cmp x y ≠ Ordering.gt ↔ cmp y x ≠ Ordering.lt

theorem Std.TransCmp.le_trans {α : Type u_1} {cmp : α → α → Ordering} [TransCmp cmp] {x y z : α} : cmp x y ≠ Ordering.gt → cmp y z ≠ Ordering.gt → cmp 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.lt → cmp y z ≠ Ordering.gt → cmp 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.gt → cmp y z = Ordering.lt → cmp x z = Ordering.lt

theorem Std.TransCmp.ge_trans {α : Type u_1} {cmp : α → α → Ordering} [TransCmp cmp] {x y z : α} : cmp x y ≠ Ordering.lt → cmp y z ≠ Ordering.lt → cmp 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.gt → cmp y z ≠ Ordering.lt → cmp 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.lt → cmp y z = Ordering.gt → cmp x z = Ordering.gt

class Std.LawfulLTCmp {α : Type u_1} [LT α] (cmp : α → α → Ordering) extends Std.OrientedCmp cmp : Prop

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.

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

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.

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

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

• eq_swap {a b : α} : cmp a b = (cmp b a).swap
• isLE_trans {a b c : α} : (cmp a b).isLE = true → (cmp b c).isLE = true → (cmp a c).isLE = true
• compare_eq_iff_beq {a b : α} : cmp a b = Ordering.eq ↔ (a == b) = true
• eq_lt_iff_lt {x y : α} : cmp x y = Ordering.lt ↔ x < y
• isLE_iff_le {x y : α} : (cmp x y).isLE = true ↔ x ≤ y

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

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

• eq_swap {a b : α} : cmp a b = (cmp b a).swap
• isLE_trans {a b c : α} : (cmp a b).isLE = true → (cmp b c).isLE = true → (cmp a c).isLE = true
• compare_self {a : α} : cmp a a = Ordering.eq
• eq_of_compare {a b : α} : cmp a b = Ordering.eq → a = b
• eq_lt_iff_lt {x y : α} : cmp x y = Ordering.lt ↔ x < y
• isLE_iff_le {x y : α} : (cmp x y).isLE = true ↔ x ≤ y

@[reducible, inline]

abbrev Std.LawfulLTOrd (α : Type u_1) [LT α] [Ord α] : Prop

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

Equations

• Std.LawfulLTOrd α = Std.LawfulLTCmp compare

@[reducible, inline]

abbrev Std.LawfulLEOrd (α : Type u_1) [LE α] [Ord α] : Prop

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

Equations

• Std.LawfulLEOrd α = Std.LawfulLECmp compare

@[reducible, inline]

abbrev Std.LawfulBOrd (α : Type u_1) [LE α] [LT α] [BEq α] [Ord α] : Prop

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

Equations

• Std.LawfulBOrd α = Std.LawfulBCmp compare

@[reducible, inline]

abbrev Std.LawfulOrd (α : Type u_1) [LE α] [LT α] [Ord α] : Prop

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

Equations

• Std.LawfulOrd α = Std.LawfulCmp compare

instance Std.instOrientedCmpFlipOrdering_batteries {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} [inst : OrientedCmp cmp] : OrientedCmp (flip cmp)

instance Std.instTransCmpFlipOrdering_batteries {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} [inst : TransCmp cmp] : TransCmp (flip cmp)

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

instance Std.instTransCmpByKey {α : Type u_1} {β : Type u_2} (f : α → β) (cmp : β → β → Ordering) [TransCmp cmp] : TransCmp (Ordering.byKey f 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 : α → β) : OrientedCmp (compareOn f)

instance Std.instTransCmpCompareOnOfTransOrd_batteries {β : Type u_1} {α : Type u_2} [Ord β] [TransOrd β] (f : α → β) : TransCmp (compareOn f)

theorem Std.OrientedOrd.instOn {β : Type u_1} {α : Type u_2} [ord : Ord β] [OrientedOrd β] (f : α → β) : OrientedOrd α

theorem Std.TransOrd.instOn {β : Type u_1} {α : Type u_2} [ord : Ord β] [TransOrd β] (f : α → β) : TransOrd α

theorem Std.OrientedOrd.instOrdLex' {α : Type u_1} (ord₁ ord₂ : Ord α) [OrientedOrd α] [OrientedOrd α] : OrientedOrd α

theorem Std.TransOrd.instOrdLex' {α : Type u_1} (ord₁ ord₂ : Ord α) [TransOrd α] [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 < y → y < z → x < z) (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = 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 < y → y < z → x < z) (not_lt : ∀ {x y : α}, ¬x < y → y ≤ x) (le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = 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 < y → y < z → x < z) (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = 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 < y → y < z → x < z) (not_lt : ∀ {x y : α}, ¬x < y → y ≤ x) (le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = 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 < y → y < z → x < z) (not_lt : ∀ {x y : α}, ¬x < y ↔ y ≤ x) (le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = 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 < y → y < z → x < z) (not_lt : ∀ {x y : α}, ¬x < y ↔ y ≤ x) (le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) : LawfulCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2

instance Std.instLawfulOrdNat : LawfulOrd Nat

instance Std.instLawfulOrdInt : LawfulOrd Int

instance Std.instLawfulOrdBool : LawfulOrd Bool

instance Std.instLawfulOrdFin {n : Nat} : LawfulOrd (Fin n)