Documentation

Mathlib.Deprecated.AlgebraClasses

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.

source
@[deprecated]
class IsLeftCancel (α : Sort u) (op : α → α → α) :
Prop
  • left_cancel (a b c : α) : op a b = op a c → b = c
Instances
    source
    @[deprecated]
    class IsRightCancel (α : Sort u) (op : α → α → α) :
    Prop
    • right_cancel (a b c : α) : op a b = op c b → a = c
    Instances
      source
      @[deprecated]
      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
      Instances
        source
        @[instance 100]
        instance isTotalPreorder_isPreorder (α : Sort u) (r : α → α → Prop) [s : IsTotalPreorder α r] :
        IsPreorder α r

        Every total pre-order is a pre-order.

        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.

        Instances
          source
          @[deprecated, instance 100]
          instance instIsIncompTransOfIsStrictWeakOrder (α : Sort u) (lt : α → α → Prop) [IsStrictWeakOrder α lt] :
          IsIncompTrans α lt
          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
            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.
            Instances For
              source
              @[deprecated]
              theorem isStrictWeakOrder_of_isTotalPreorder {α : Sort u} {le 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
              source
              @[deprecated]
              instance isStrictWeakOrder_of_linearOrder {α : Type u_1} [LinearOrder α] :
              IsStrictWeakOrder α fun (x1 x2 : α) => x1 < x2
              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