Deprecated Batteries comparison classes

Examples are to ensure that old instances have equivalent new instances.

@[deprecated Std.OrientedCmp (since := "2025-07-01")]

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

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

• symm (x y : α) : (cmp x y).swap = 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.

@[deprecated Std.OrientedCmp.gt_iff_lt (since := "2025-07-01")]

theorem Batteries.OrientedCmp.cmp_eq_gt {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x y : α✝} [OrientedCmp cmp] : cmp x y = Ordering.gt ↔ cmp y x = Ordering.lt

@[deprecated Std.OrientedCmp.le_iff_ge (since := "2025-07-01")]

theorem Batteries.OrientedCmp.cmp_ne_gt {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x y : α✝} [OrientedCmp cmp] : cmp x y ≠ Ordering.gt ↔ cmp y x ≠ Ordering.lt

@[deprecated Std.OrientedCmp.eq_comm (since := "2025-07-01")]

theorem Batteries.OrientedCmp.cmp_eq_eq_symm {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x y : α✝} [OrientedCmp cmp] : cmp x y = Ordering.eq ↔ cmp y x = Ordering.eq

@[deprecated Std.ReflCmp.compare_self (since := "2025-07-01")]

theorem Batteries.OrientedCmp.cmp_refl {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x : α✝} [OrientedCmp cmp] : cmp x x = Ordering.eq

@[deprecated Std.OrientedCmp.not_lt_of_lt (since := "2025-07-01")]

theorem Batteries.OrientedCmp.lt_asymm {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x y : α✝} [OrientedCmp cmp] (h : cmp x y = Ordering.lt) : cmp y x ≠ Ordering.lt

@[deprecated Std.OrientedCmp.not_gt_of_gt (since := "2025-07-01")]

theorem Batteries.OrientedCmp.gt_asymm {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x y : α✝} [OrientedCmp cmp] (h : cmp x y = Ordering.gt) : cmp y x ≠ Ordering.gt

@[deprecated Std.TransCmp (since := "2025-07-01")]

class Batteries.TransCmp {α : Sort u_1} (cmp : α → α → Ordering) extends Batteries.OrientedCmp cmp : Prop

TransCmp cmp asserts that cmp induces a transitive relation.

• symm (x y : α) : (cmp x y).swap = 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.

@[deprecated Std.TransCmp.ge_trans (since := "2025-07-01")]

theorem Batteries.TransCmp.ge_trans {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [TransCmp cmp] {x y z : α✝} (h₁ : cmp x y ≠ Ordering.lt) (h₂ : cmp y z ≠ Ordering.lt) : cmp x z ≠ Ordering.lt

@[deprecated Std.TransCmp.lt_of_le_of_lt (since := "2025-07-01")]

theorem Batteries.TransCmp.le_lt_trans {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [TransCmp cmp] {x y z : α✝} (h₁ : cmp x y ≠ Ordering.gt) (h₂ : cmp y z = Ordering.lt) : cmp x z = Ordering.lt

@[deprecated Std.TransCmp.lt_of_lt_of_le (since := "2025-07-01")]

theorem Batteries.TransCmp.lt_le_trans {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [TransCmp cmp] {x y z : α✝} (h₁ : cmp x y = Ordering.lt) (h₂ : cmp y z ≠ Ordering.gt) : cmp x z = Ordering.lt

@[deprecated Std.TransCmp.lt_trans (since := "2025-07-01")]

theorem Batteries.TransCmp.lt_trans {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [TransCmp cmp] {x y z : α✝} (h₁ : cmp x y = Ordering.lt) (h₂ : cmp y z = Ordering.lt) : cmp x z = Ordering.lt

@[deprecated Std.TransCmp.gt_trans (since := "2025-07-01")]

theorem Batteries.TransCmp.gt_trans {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [TransCmp cmp] {x y z : α✝} (h₁ : cmp x y = Ordering.gt) (h₂ : cmp y z = Ordering.gt) : cmp x z = Ordering.gt

@[deprecated Std.TransCmp.congr_left (since := "2025-07-01")]

theorem Batteries.TransCmp.cmp_congr_left {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [TransCmp cmp] {x y z : α✝} (xy : cmp x y = Ordering.eq) : cmp x z = cmp y z

@[deprecated Std.TransCmp.congr_left (since := "2025-07-01")]

theorem Batteries.TransCmp.cmp_congr_left' {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [TransCmp cmp] {x y : α✝} (xy : cmp x y = Ordering.eq) : cmp x = cmp y

@[deprecated Std.TransCmp.congr_right (since := "2025-07-01")]

theorem Batteries.TransCmp.cmp_congr_right {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [TransCmp cmp] {y z x : α✝} (yz : cmp y z = Ordering.eq) : cmp x y = cmp x z

instance Batteries.instOrientedCmpFlipOrdering {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [inst : OrientedCmp cmp] : OrientedCmp (flip cmp)

instance Batteries.instTransCmpFlipOrdering {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [inst : TransCmp cmp] : TransCmp (flip cmp)

@[deprecated Std.LawfulBEqCmp (since := "2025-07-01")]

class Batteries.BEqCmp {α : Type u_1} [BEq α] (cmp : α → α → Ordering) : Prop

BEqCmp cmp asserts that cmp x y = .eq and x == y coincide.

• cmp_iff_beq {x y : α} : cmp x y = Ordering.eq ↔ (x == y) = true

  cmp x y = .eq holds iff x == y is true.

@[deprecated Std.LawfulEqCmp.compare_eq_iff_eq (since := "2025-07-01")]

theorem Batteries.BEqCmp.cmp_iff_eq {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [BEq α] [LawfulBEq α] [BEqCmp cmp] : cmp x y = Ordering.eq ↔ x = y

@[deprecated Std.LawfulLTCmp (since := "2025-07-01")]

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

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

• symm (x y : α) : (cmp x y).swap = cmp y x
• cmp_iff_lt {x y : α} : cmp x y = Ordering.lt ↔ x < y

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

@[deprecated Std.LawfulLTCmp.eq_gt_iff_gt (since := "2025-07-01")]

theorem Batteries.LTCmp.cmp_iff_gt {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [LT α] [LTCmp cmp] : cmp x y = Ordering.gt ↔ y < x

@[deprecated Std.LawfulLECmp (since := "2025-07-01")]

class Batteries.LECmp {α : Type u_1} [LE α] (cmp : α → α → Ordering) extends Batteries.OrientedCmp cmp : Prop

LECmp cmp asserts that cmp x y ≠ .gt and x ≤ y coincide.

• symm (x y : α) : (cmp x y).swap = cmp y x
• cmp_iff_le {x y : α} : cmp x y ≠ Ordering.gt ↔ x ≤ y

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

@[deprecated Std.LawfulLECmp.ne_lt_iff_ge (since := "2025-07-01")]

theorem Batteries.LECmp.cmp_iff_ge {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [LE α] [LECmp cmp] : cmp x y ≠ Ordering.lt ↔ y ≤ x

@[deprecated Std.LawfulBCmp (since := "2025-07-01")]

class Batteries.LawfulCmp {α : Type u_1} [LE α] [LT α] [BEq α] (cmp : α → α → Ordering) extends Batteries.TransCmp cmp, Batteries.BEqCmp cmp, Batteries.LTCmp cmp, Batteries.LECmp cmp : Prop

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

• symm (x y : α) : (cmp x y).swap = cmp y x
• le_trans {x y z : α} : cmp x y ≠ Ordering.gt → cmp y z ≠ Ordering.gt → cmp x z ≠ Ordering.gt
• cmp_iff_beq {x y : α} : cmp x y = Ordering.eq ↔ (x == y) = true
• cmp_iff_lt {x y : α} : cmp x y = Ordering.lt ↔ x < y
• cmp_iff_le {x y : α} : cmp x y ≠ Ordering.gt ↔ x ≤ y

@[reducible, inline, deprecated Std.OrientedOrd (since := "2025-07-01")]

abbrev Batteries.OrientedOrd (α : Type u_1) [Ord α] : Prop

OrientedOrd α asserts that the Ord instance satisfies OrientedCmp.

Equations

• Batteries.OrientedOrd α = Batteries.OrientedCmp compare

@[reducible, inline, deprecated Std.TransOrd (since := "2025-07-01")]

abbrev Batteries.TransOrd (α : Type u_1) [Ord α] : Prop

TransOrd α asserts that the Ord instance satisfies TransCmp.

Equations

• Batteries.TransOrd α = Batteries.TransCmp compare

@[reducible, inline, deprecated Std.LawfulBEqOrd (since := "2025-07-01")]

abbrev Batteries.BEqOrd (α : Type u_1) [BEq α] [Ord α] : Prop

BEqOrd α asserts that the Ord and BEq instances are coherent via BEqCmp.

Equations

• Batteries.BEqOrd α = Batteries.BEqCmp compare

@[reducible, inline, deprecated Std.LawfulLTOrd (since := "2025-07-01")]

abbrev Batteries.LTOrd (α : Type u_1) [LT α] [Ord α] : Prop

LTOrd α asserts that the Ord instance satisfies LTCmp.

Equations

• Batteries.LTOrd α = Batteries.LTCmp compare

@[reducible, inline, deprecated Std.LawfulLEOrd (since := "2025-07-01")]

abbrev Batteries.LEOrd (α : Type u_1) [LE α] [Ord α] : Prop

LEOrd α asserts that the Ord instance satisfies LECmp.

Equations

• Batteries.LEOrd α = Batteries.LECmp compare

@[reducible, inline, deprecated Std.LawfulBOrd (since := "2025-07-01")]

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

LawfulOrd α asserts that the Ord instance satisfies LawfulCmp.

Equations

• Batteries.LawfulOrd α = Batteries.LawfulCmp compare

@[deprecated Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm (since := "2025-07-01")]

theorem Batteries.TransCmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [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

@[deprecated Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm (since := "2025-07-01")]

theorem Batteries.TransCmp.compareOfLessAndEq_of_le {α : Type u_1} [LT α] [LE α] [DecidableRel LT.lt] [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

@[deprecated Std.LawfulBEqCmp.compareOfLessAndEq_of_lt_irrefl (since := "2025-07-01")]

theorem Batteries.BEqCmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [DecidableEq α] [BEq α] [LawfulBEq α] (lt_irrefl : ∀ (x : α), ¬x < x) : BEqCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2

@[deprecated Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm (since := "2025-07-01")]

theorem Batteries.LTCmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [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) : LTCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2

@[deprecated Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm (since := "2025-07-01")]

theorem Batteries.LTCmp.compareOfLessAndEq_of_le {α : Type u_1} [LT α] [DecidableRel LT.lt] [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) : LTCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2

@[deprecated Std.LawfulLECmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm (since := "2025-07-01")]

theorem Batteries.LECmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [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) : LECmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2

@[deprecated Std.LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm (since := "2025-07-01")]

theorem Batteries.LawfulCmp.compareOfLessAndEq {α : Type u_1} [LT α] [DecidableRel LT.lt] [DecidableEq α] [BEq α] [LawfulBEq α] [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) : LawfulCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2

@[deprecated Std.LawfulLTCmp.eq_compareOfLessAndEq (since := "2025-07-01")]

theorem Batteries.LTCmp.eq_compareOfLessAndEq {α : Type u_1} {cmp : α → α → Ordering} [LT α] [DecidableEq α] [BEq α] [LawfulBEq α] [BEqCmp cmp] [LTCmp cmp] (x y : α) [Decidable (x < y)] : cmp x y = compareOfLessAndEq x y

instance Batteries.instOrientedCmpCompareLex {α✝ : Sort u_1} {cmp₁ cmp₂ : α✝ → α✝ → Ordering} [inst₁ : OrientedCmp cmp₁] [inst₂ : OrientedCmp cmp₂] : OrientedCmp (compareLex cmp₁ cmp₂)

instance Batteries.instTransCmpCompareLex {α✝ : Sort u_1} {cmp₁ cmp₂ : α✝ → α✝ → Ordering} [inst₁ : TransCmp cmp₁] [inst₂ : TransCmp cmp₂] : TransCmp (compareLex cmp₁ cmp₂)

instance Batteries.instOrientedCmpCompareOnOfOrientedOrd {β : Type u_1} {α : Sort u_2} [Ord β] [OrientedOrd β] (f : α → β) : OrientedCmp (compareOn f)

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

@[deprecated "instance exists" (since := "2025-07-01")]

theorem Batteries.OrientedOrd.instLexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [OrientedOrd α] [OrientedOrd β] : OrientedOrd (α × β)

Local instance for OrientedOrd lexOrd.

@[deprecated "instance exists" (since := "2025-07-01")]

theorem Batteries.TransOrd.instLexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [TransOrd α] [TransOrd β] : TransOrd (α × β)

Local instance for TransOrd lexOrd.

@[deprecated Std.OrientedOrd.opposite (since := "2025-07-01")]

theorem Batteries.OrientedOrd.instOpposite {α : Type u_1} [ord : Ord α] [inst : OrientedOrd α] : OrientedOrd α

Local instance for OrientedOrd ord.opposite.

@[deprecated Std.TransOrd.opposite (since := "2025-07-01")]

theorem Batteries.TransOrd.instOpposite {α : Type u_1} [ord : Ord α] [inst : TransOrd α] : TransOrd α

Local instance for TransOrd ord.opposite.

@[deprecated Std.OrientedOrd.instOn (since := "2025-07-01")]

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

Local instance for OrientedOrd (ord.on f).

@[deprecated Std.TransOrd.instOn (since := "2025-07-01")]

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

Local instance for TransOrd (ord.on f).

@[deprecated "instance exists" (since := "2025-07-01")]

theorem Batteries.OrientedOrd.instOrdLex {α : Type u_1} {β : Type u_2} [oα : Ord α] [oβ : Ord β] [OrientedOrd α] [OrientedOrd β] : OrientedOrd (α × β)

Local instance for OrientedOrd (oα.lex oβ).

@[deprecated "instance exists" (since := "2025-07-01")]

theorem Batteries.TransOrd.instOrdLex {α : Type u_1} {β : Type u_2} [oα : Ord α] [oβ : Ord β] [TransOrd α] [TransOrd β] : TransOrd (α × β)

Local instance for TransOrd (oα.lex oβ).

@[deprecated Std.OrientedOrd.instOrdLex' (since := "2025-07-01")]

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

Local instance for OrientedOrd (oα.lex' oβ).

@[deprecated Std.TransOrd.instOrdLex' (since := "2025-07-01")]

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

Local instance for TransOrd (oα.lex' oβ).