Documentation

Mathlib.Init.Algebra.Classes

Note about Mathlib/Init/ #

The files in Mathlib/Init are leftovers from the port from Mathlib3. (They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main Mathlib directory structure. Contributions assisting with this are appreciated.

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.

source
@[deprecated]
class IsLeftCancel (α : Sort u) (op : α → α → α) :
Prop
  • left_cancel : ∀ (a b c : α), op a b = op a c → b = c
Instances
source
theorem IsLeftCancel.left_cancel {α : Sort u} {op : α → α → α} [self : IsLeftCancel α op] (a : α) (b : α) (c : α) :
op a b = op a c → b = c
source
@[deprecated]
class IsRightCancel (α : Sort u) (op : α → α → α) :
Prop
  • right_cancel : ∀ (a b c : α), op a b = op c b → a = c
Instances
source
theorem IsRightCancel.right_cancel {α : Sort u} {op : α → α → α} [self : IsRightCancel α op] (a : α) (b : α) (c : α) :
op a b = op c b → a = c
source
@[deprecated]
class IsTotalPreorder (α : Sort u) (r : α → α → Prop) extends IsTrans , IsTotal :
Prop

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

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

    Every total pre-order is a pre-order.

    Equations
    • ⋯ = ⋯
    source
    @[deprecated]
    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
    Instances
    source
    theorem IsIncompTrans.incomp_trans {α : Sort u} {lt : α → α → Prop} [self : IsIncompTrans α lt] (a : α) (b : α) (c : α) :
    ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a
    source
    @[deprecated, instance 100]
    instance instIsIncompTransOfIsStrictWeakOrder (α : Sort u) (lt : α → α → Prop) [IsStrictWeakOrder α lt] :
    IsIncompTrans α lt
    Equations
    • ⋯ = ⋯
    source
    @[deprecated]
    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
    source
    @[elab_without_expected_type, deprecated]
    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
    source
    @[deprecated]
    def StrictWeakOrder.Equiv {α : Sort u} {r : α → α → Prop} (a : α) (b : α) :
    Prop
    Equations
    Instances For
    source
    @[deprecated]
    theorem StrictWeakOrder.esymm {α : Sort u} {r : α → α → Prop} {a : α} {b : α} :
    StrictWeakOrder.Equiv a b → StrictWeakOrder.Equiv b a
    source
    @[deprecated]
    theorem StrictWeakOrder.not_lt_of_equiv {α : Sort u} {r : α → α → Prop} {a : α} {b : α} :
    StrictWeakOrder.Equiv a b → ¬r a b
    source
    @[deprecated]
    theorem StrictWeakOrder.not_lt_of_equiv' {α : Sort u} {r : α → α → Prop} {a : α} {b : α} :
    StrictWeakOrder.Equiv a b → ¬r b a
    source
    @[deprecated]
    theorem StrictWeakOrder.erefl {α : Sort u} {r : α → α → Prop} [IsStrictWeakOrder α r] (a : α) :
    StrictWeakOrder.Equiv a a
    source
    @[deprecated]
    theorem StrictWeakOrder.etrans {α : Sort u} {r : α → α → Prop} [IsStrictWeakOrder α r] {a : α} {b : α} {c : α} :
    StrictWeakOrder.Equiv a b → StrictWeakOrder.Equiv b c → StrictWeakOrder.Equiv a c
    source
    @[deprecated]
    instance StrictWeakOrder.isEquiv {α : Sort u} {r : α → α → Prop} [IsStrictWeakOrder α r] :
    IsEquiv α StrictWeakOrder.Equiv
    Equations
    • ⋯ = ⋯
    source
    def StrictWeakOrder.«term_≈[_]_» :
    Lean.TrailingParserDescr

    The equivalence relation induced by lt

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[deprecated]
    theorem isStrictWeakOrder_of_isTotalPreorder {α : Sort u} {le : α → α → Prop} {lt : α → α → Prop} [DecidableRel le] [IsTotalPreorder α le] (h : ∀ (a b : α), lt a b ↔ ¬le b a) :
    IsStrictWeakOrder α lt
    source
    @[deprecated]
    instance instIsTotalPreorderLe {α : Type u_1} [LinearOrder α] :
    IsTotalPreorder α fun (x1 x2 : α) => x1 ≤ x2
    Equations
    • ⋯ = ⋯
    source
    @[deprecated]
    instance isStrictWeakOrder_of_linearOrder {α : Type u_1} [LinearOrder α] :
    IsStrictWeakOrder α fun (x1 x2 : α) => x1 < x2
    Equations
    • ⋯ = ⋯
    source
    @[deprecated]
    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
    source
    @[deprecated]
    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
    source
    @[deprecated]
    theorem eq_of_incomp {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] {a : α} {b : α} :
    ¬lt a b ∧ ¬lt b a → a = b
    source
    @[deprecated]
    theorem eq_of_eqv_lt {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] {a : α} {b : α} :
    StrictWeakOrder.Equiv a b → a = b
    source
    @[deprecated]
    theorem incomp_iff_eq {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a : α) (b : α) :
    ¬lt a b ∧ ¬lt b a ↔ a = b
    source
    @[deprecated]
    theorem eqv_lt_iff_eq {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a : α) (b : α) :
    StrictWeakOrder.Equiv a b ↔ a = b