Note about deprecated files

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

Unbundled algebra classes

These classes were part of an incomplete refactor described here on the github Wiki. However a subset of them are widely used in mathlib3, and it has been tricky to clean this up as this file was in core Lean 3.

@[deprecated "No deprecation message was provided." (since := "2024-09-11")]

class IsLeftCancel (α : Sort u) (op : α → α → α) : Prop

• left_cancel (a b c : α) : op a b = op a c → b = c

@[deprecated "No deprecation message was provided." (since := "2024-09-11")]

class IsRightCancel (α : Sort u) (op : α → α → α) : Prop

• right_cancel (a b c : α) : op a b = op c b → a = c

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

class IsTotalPreorder (α : Sort u) (r : α → α → Prop) extends IsTrans α r, IsTotal α r : Prop

IsTotalPreorder X r means that the binary relation r on X is total and a preorder.

• trans (a b c : α) : r a b → r b c → r a c
• total (a b : α) : r a b ∨ r b a

@[instance 100]

instance isTotalPreorder_isPreorder (α : Sort u) (r : α → α → Prop) [s : IsTotalPreorder α r] : IsPreorder α r

Every total pre-order is a pre-order.

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

class IsIncompTrans (α : Sort u) (lt : α → α → Prop) : Prop

IsIncompTrans X lt means that for lt a binary relation on X, the incomparable relation fun a b => ¬ lt a b ∧ ¬ lt b a is transitive.

• incomp_trans (a b c : α) : ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a

@[deprecated "No deprecation message was provided." (since := "2024-07-30"), instance 100]

instance instIsIncompTransOfIsStrictWeakOrder (α : Sort u) (lt : α → α → Prop) [IsStrictWeakOrder α lt] : IsIncompTrans α lt

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem incomp_trans {α : Sort u} {r : α → α → Prop} [IsIncompTrans α r] {a b c : α} : ¬r a b ∧ ¬r b a → ¬r b c ∧ ¬r c b → ¬r a c ∧ ¬r c a

@[elab_without_expected_type, deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem incomp_trans_of {α : Sort u} (r : α → α → Prop) [IsIncompTrans α r] {a b c : α} : ¬r a b ∧ ¬r b a → ¬r b c ∧ ¬r c b → ¬r a c ∧ ¬r c a

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

def StrictWeakOrder.Equiv {α : Sort u} {r : α → α → Prop} (a b : α) : Prop

Equations

• StrictWeakOrder.Equiv a b = (¬r a b ∧ ¬r b a)

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem StrictWeakOrder.esymm {α : Sort u} {r : α → α → Prop} {a b : α} : StrictWeakOrder.Equiv a b → StrictWeakOrder.Equiv b a

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem StrictWeakOrder.not_lt_of_equiv {α : Sort u} {r : α → α → Prop} {a b : α} : StrictWeakOrder.Equiv a b → ¬r a b

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem StrictWeakOrder.not_lt_of_equiv' {α : Sort u} {r : α → α → Prop} {a b : α} : StrictWeakOrder.Equiv a b → ¬r b a

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem StrictWeakOrder.erefl {α : Sort u} {r : α → α → Prop} [IsStrictWeakOrder α r] (a : α) : StrictWeakOrder.Equiv a a

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem StrictWeakOrder.etrans {α : Sort u} {r : α → α → Prop} [IsStrictWeakOrder α r] {a b c : α} : StrictWeakOrder.Equiv a b → StrictWeakOrder.Equiv b c → StrictWeakOrder.Equiv a c

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

instance StrictWeakOrder.isEquiv {α : Sort u} {r : α → α → Prop} [IsStrictWeakOrder α r] : IsEquiv α StrictWeakOrder.Equiv

def StrictWeakOrder.«term_≈[_]_» : Lean.TrailingParserDescr

The equivalence relation induced by lt

Equations

• One or more equations did not get rendered due to their size.

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem isStrictWeakOrder_of_isTotalPreorder {α : Sort u} {le lt : α → α → Prop} [DecidableRel le] [IsTotalPreorder α le] (h : ∀ (a b : α), lt a b ↔ ¬le b a) : IsStrictWeakOrder α lt

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

instance instIsTotalPreorderLe {α : Type u_1} [LinearOrder α] : IsTotalPreorder α fun (x1 x2 : α) => x1 ≤ x2

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

instance isStrictWeakOrder_of_linearOrder {α : Type u_1} [LinearOrder α] : IsStrictWeakOrder α fun (x1 x2 : α) => x1 < x2

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem lt_of_lt_of_incomp {α : Sort u} {lt : α → α → Prop} [IsStrictWeakOrder α lt] [DecidableRel lt] {a b c : α} : lt a b → ¬lt b c ∧ ¬lt c b → lt a c

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem lt_of_incomp_of_lt {α : Sort u} {lt : α → α → Prop} [IsStrictWeakOrder α lt] [DecidableRel lt] {a b c : α} : ¬lt a b ∧ ¬lt b a → lt b c → lt a c

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem eq_of_incomp {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] {a b : α} : ¬lt a b ∧ ¬lt b a → a = b

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem eq_of_eqv_lt {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] {a b : α} : StrictWeakOrder.Equiv a b → a = b

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem incomp_iff_eq {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a b : α) : ¬lt a b ∧ ¬lt b a ↔ a = b

@[deprecated "No deprecation message was provided." (since := "2024-07-30")]

theorem eqv_lt_iff_eq {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a b : α) : StrictWeakOrder.Equiv a b ↔ a = b