Green's Relations Definitions

This file defines Green's preorders and equivalence relations on semigroups.

We prove basic theorems, like Semigroup.rEquiv_lEquiv_comm, which are necessary for instantiating DEquiv as an equivalence relation with Semigroup.DEquiv.isEquivalence.

We also prove simp lemmas at the end of the file.

Main definitions

In the following definitions, S is a semigroup and x y : S.

Green's Preorder Relations

• Semigroup.RPreorder - x is 𝓡-below y (notated x ≤𝓡 y) iff there exists a z : WithOne S such that ↑x = ↑y * z

• Semigroup.LPreorder - x is 𝓛-below y (notated x ≤𝓛 y) iff there exists a z : WithOne S such that ↑x = z * ↑y

• Semigroup.JPreorder - x is 𝓙-below y (notated x ≤𝓙 y) iff there exists z w : WithOne S such that ↑x = z * ↑y * w

• Semigroup.HPreorder - x is 𝓗-below y (notated x ≤𝓗 y) iff x ≤𝓛 y and x ≤𝓡 y

We instantiate each preorder in the unbundled IsPreorder Class:

• Semigroup.RPreorder.isPreorder - instance for [IsPreorder S RPreorder]
• Semigroup.LPreorder.isPreorder - instance for [IsPreorder S LPreorder]
• Semigroup.JPreorder.isPreorder - instance for [IsPreorder S JPreorder]
• Semigroup.HPreorder.isPreorder - instance for [IsPreorder S HPreorder]

Green's Equivalence Relations

We define the 𝓡, 𝓛, 𝓙, 𝓗 relations as the symmetric closure of their corresponding preorders:

• Semigroup.REquiv - x 𝓡 y iff x ≤𝓡 y and y ≤𝓡 x
• Semigroup.LEquiv - x 𝓛 y iff x ≤𝓛 y and y ≤𝓛 x
• Semigroup.JEquiv - x 𝓙 y iff x ≤𝓙 y and y ≤𝓙 x
• Semigroup.HEquiv - x 𝓗 y iff x ≤𝓗 y and y ≤𝓗 x

The 𝓓 relation is defined as the composition of 𝓡 and 𝓛:

• Semigroup.DEquiv - x 𝓓 y iff ∃ z, x 𝓡 z ∧ z 𝓛 y

Equivalence classes of elements as sets:

• Semigroup.REquiv.set - Notated ⟦x⟧𝓡, the Set S of elements 𝓡-related to x
• Semigroup.LEquiv.set - Notated ⟦x⟧𝓛, the Set S of elements 𝓛-related to x
• Semigroup.JEquiv.set - Notated ⟦x⟧𝓙, the Set S of elements 𝓙-related to x
• Semigroup.HEquiv.set - Notated ⟦x⟧𝓗, the Set S of elements 𝓗-related to x
• Semigroup.DEquiv.set - Notated ⟦x⟧𝓓, the Set S of elements 𝓓-related to x

Main theorems

• IsPreorder.SymmClosure - Given a preorder α : S → S → Prop and an instance [IsPreorder S α], the symmetric closure of α is an equivalence relation.

We use the preceding theorem to prove that 𝓡, 𝓛, 𝓙, 𝓗 are equivalence relations.

• Semigroup.REquiv.isEquivalence
• Semigroup.LEquiv.isEquivalence
• Semigroup.JEquiv.isEquivalence
• Semigroup.HEquiv.isEquivalence

We prove that ≤𝓡 and 𝓡 are compatible with left multiplication. That is, if x (≤)𝓡 y, then z * x (≤)𝓡 z * y. We also prove that ≤𝓛 and 𝓛 are compatible with right multiplication:

• Semigroup.RPreorder.lmult_compat

• Semigroup.REquiv.lmult_compat

• Semigroup.LPreorder.rmult_compat

• Semigroup.LEquiv.rmult_compat

• Semigroup.rEquiv_lEquiv_comm - We prove that 𝓡 and 𝓛 commute under composition, i.e. (∃ z, x 𝓡 z ∧ z 𝓛 y) ↔ (∃ z, x 𝓛 z ∧ z 𝓡 y). This allows us to prove that 𝓓 is symmetric.

We prove that 𝓓 is closed under composition with 𝓛 and 𝓡. This allows us to prove that 𝓓 is transitive:

• Semigroup.DEquiv.closed_under_lEquiv - If x 𝓓 y and y 𝓛 z, then x 𝓓 z.

• Semigroup.DEquiv.closed_under_rEquiv - If x 𝓓 y and y 𝓡 z, then x 𝓓 z.

• Semigroup.DEquiv.isEquivalence - The 𝓓 relation is reflexive, symmetric, and transitive.

Implementation notes

Because we defined 𝓗 as the symmetric closure of ≤𝓗, using simp [HEquiv] will change x 𝓗 y to x ≤𝓗 y ∧ y ≤𝓗 x. If you want to rewrite to x 𝓡 y ∧ x 𝓛 y, use HEquiv.iff_rEquiv_and_lEquiv.

The simp-tagged lemmas at the end of the file are able to close goals like x * y ≤𝓡 x by calling simp. Also, if you have a goal like x 𝓙 y, and a local hypothesis hr : x 𝓡 y, you can close this goal by simp [hr] or simp_all.

We also define two lemmas, le and ge, in the namespaces for 𝓡, 𝓛, 𝓙, 𝓗. These lemmas restrict hypotheses about equivalences to hypotheses about preorders. For example, if you have the goal x ≤𝓡 y and a hypothesis h : x 𝓡 y, you can close that goal with exact h.le. Similarly, if the goal is y ≤𝓡 x, you can use exact h.ge.

References

TODO

Blueprint

• One blueprint DEF entry for Green's Preorders and Equivalence Relations. Label : greens-relations Tagged Lean defs :

  • Semigroup.RPreorder
  • Semigroup.LPreorder
  • Semigroup.JPreorder
  • Semigroup.HPreorder
  • Semigroup.RPreorder.isPreorder
  • Semigroup.LPreorder.isPreorder
  • Semigroup.JPreorder.isPreorder
  • Semigroup.HPreorder.isPreorder
  • Semigroup.REquiv
  • Semigroup.LEquiv
  • Semigroup.JEquiv
  • Semigroup.HEquiv
  • Semigroup.DEquiv
  • Semigroup.REquiv.isEquivalence
  • Semigroup.LEquiv.isEquivalence
  • Semigroup.JEquiv.isEquivalence
  • Semigroup.HEquiv.isEquivalence
  • Semigroup.DEquiv.isEquivalence Content :
  • Explain definitions of the relations
  • introduce notation for preorders, equivalence, and equivalence classes
  • Explain that the preorders are reflexive and transitive (preorders)
  • Explain that the equivalences are reflexive, symmetric, and transitive (equivalence relations) Dependencies : None

• One Lemma entry for the right/left mul compatibility lemmas. Label : greens-relations-mul-compat tagged lean lemmas :

  • Semigroup.RPreorder.lmult_compat
  • Semigroup.REquiv.lmult_compat
  • Semigroup.LPreorder.rmult_compat
  • Semigroup.LEquiv.rmult_compat Content : Prove it for ≤𝓡, then for 𝓡, then say a similar arguement holds for ≤𝓛 and 𝓛 Dependencies : greens-relations

• One Lemma entry for the commutation of 𝓡 and 𝓛. Label : r-l-comm tagged lean lemmas :

  • Semigroup.rEquiv_lEquiv_comm Content : Prove it and mention that this is used to prove that 𝓓 is symmetric. Dependencies : greens-relations-mul-compat

• One Lemma entry for the closure of 𝓓 under 𝓡 and 𝓛. label : d-equiv-closed tagged lean lemmas :

  • Semigroup.DEquiv.closed_under_lEquiv
  • Semigroup.DEquiv.closed_under_rEquiv Content : Prove closure under 𝓛, then say a similar argument holds for closure under 𝓡. Dependencies : greens-relations

Green's Preorders

def Semigroup.RPreorder {S : Type u_1} [Semigroup S] (x y : S) : Prop

x is 𝓡-below y if x = y or there exists a z : S such that x = y * z

Equations

• (x ≤𝓡 y) = ∃ (z : WithOne S), ↑x = ↑y * z

def Semigroup.«term_≤𝓡_» : Lean.TrailingParserDescr

Equations

• Semigroup.«term_≤𝓡_» = Lean.ParserDescr.trailingNode `Semigroup.«term_≤𝓡_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤𝓡 ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem Semigroup.RPreorder.refl {S : Type u_1} [Semigroup S] (x : S) : x ≤𝓡 x

theorem Semigroup.RPreorder.trans {S : Type u_1} [Semigroup S] {x y z : S} (hxy : x ≤𝓡 y) (hyz : y ≤𝓡 z) : x ≤𝓡 z

instance Semigroup.RPreorder.isPreorder {S : Type u_1} [Semigroup S] : IsPreorder S RPreorder

≤𝓡 is a Preorder

def Semigroup.LPreorder {S : Type u_1} [Semigroup S] (x y : S) : Prop

x is 𝓛-below y if x = y or there exists a z : S such that x = z * y

Equations

• (x ≤𝓛 y) = ∃ (z : WithOne S), ↑x = z * ↑y

def Semigroup.«term_≤𝓛_» : Lean.TrailingParserDescr

Equations

• Semigroup.«term_≤𝓛_» = Lean.ParserDescr.trailingNode `Semigroup.«term_≤𝓛_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤𝓛 ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem Semigroup.LPreorder.refl {S : Type u_1} [Semigroup S] (x : S) : x ≤𝓛 x

theorem Semigroup.LPreorder.trans {S : Type u_1} [Semigroup S] {x y z : S} (hxy : x ≤𝓛 y) (hyz : y ≤𝓛 z) : x ≤𝓛 z

instance Semigroup.LPreorder.isPreorder {S : Type u_1} [Semigroup S] : IsPreorder S LPreorder

≤𝓛 is a Preorder

def Semigroup.JPreorder {S : Type u_1} [Semigroup S] (x y : S) : Prop

x is 𝓙-below y if there exists w v : WithOne S such that ↑x = w * ↑y * v

Equations

• (x ≤𝓙 y) = ∃ (w : WithOne S), ∃ (v : WithOne S), ↑x = w * ↑y * v

def Semigroup.«term_≤𝓙_» : Lean.TrailingParserDescr

Equations

• Semigroup.«term_≤𝓙_» = Lean.ParserDescr.trailingNode `Semigroup.«term_≤𝓙_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤𝓙 ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem Semigroup.JPreorder.refl {S : Type u_1} [Semigroup S] (x : S) : x ≤𝓙 x

theorem Semigroup.JPreorder.trans {S : Type u_1} [Semigroup S] {x y z : S} (hxy : x ≤𝓙 y) (hyz : y ≤𝓙 z) : x ≤𝓙 z

instance Semigroup.JPreorder.isPreorder {S : Type u_1} [Semigroup S] : IsPreorder S JPreorder

The 𝓙-preorder is a preorder.

def Semigroup.HPreorder {S : Type u_1} [Semigroup S] (x y : S) : Prop

x is 𝓗-below y if x ≤𝓡 y and x ≤𝓛 y

Equations

• (x ≤𝓗 y) = (x ≤𝓡 y ∧ x ≤𝓛 y)

def Semigroup.«term_≤𝓗_» : Lean.TrailingParserDescr

Equations

• Semigroup.«term_≤𝓗_» = Lean.ParserDescr.trailingNode `Semigroup.«term_≤𝓗_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤𝓗 ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem Semigroup.HPreorder.refl {S : Type u_1} [Semigroup S] (x : S) : x ≤𝓗 x

theorem Semigroup.HPreorder.trans {S : Type u_1} [Semigroup S] {x y z : S} (hxy : x ≤𝓗 y) (hyz : y ≤𝓗 z) : x ≤𝓗 z

instance Semigroup.HPreorder.isPreorder {S : Type u_1} [Semigroup S] : IsPreorder S HPreorder

≤𝓗 is a Preorder

Green's Equivalences (except 𝓓)

def IsPreorder.SymmClosure {α : Type u_1} (p : α → α → Prop) [h : IsPreorder α p] : Equivalence fun (x y : α) => p x y ∧ p y x

The symmetric closure of a preorder is an equivalence relation.

Equations

• ⋯ = ⋯

def Semigroup.REquiv {S : Type u_1} [Semigroup S] (x y : S) : Prop

Green's 𝓡 equivalence relation: the symmetric closure of the 𝓡-preorder.

Equations

• (x 𝓡 y) = (x ≤𝓡 y ∧ y ≤𝓡 x)

def Semigroup.term_𝓡_ : Lean.TrailingParserDescr

Equations

• Semigroup.term_𝓡_ = Lean.ParserDescr.trailingNode `Semigroup.term_𝓡_ 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " 𝓡 ") (Lean.ParserDescr.cat `term 50))

theorem Semigroup.REquiv.isEquivalence {S : Type u_1} [Semigroup S] : Equivalence fun (x y : S) => x 𝓡 y

The 𝓡 relation is an equivalence relation.

@[simp]

theorem Semigroup.REquiv.refl {S : Type u_1} [Semigroup S] (x : S) : x 𝓡 x

@[simp]

theorem Semigroup.REquiv.symm {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓡 y) : y 𝓡 x

theorem Semigroup.REquiv.trans {S : Type u_1} [Semigroup S] {x y z : S} (h₁ : x 𝓡 y) (h₂ : y 𝓡 z) : x 𝓡 z

def Semigroup.REquiv.set {S : Type u_1} [Semigroup S] (x : S) : Set S

The set of all elements 𝓡-related to x.

Equations

• ⟦x⟧𝓡 = {y : S | y 𝓡 x}

def Semigroup.REquiv.«term⟦_⟧𝓡» : Lean.ParserDescr

Equations

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

@[simp]

theorem Semigroup.REquiv.set_refl {S : Type u_1} [Semigroup S] (x : S) : x ∈ ⟦x⟧𝓡

def Semigroup.LEquiv {S : Type u_1} [Semigroup S] (x y : S) : Prop

Green's 𝓛 equivalence relation: the symmetric closure of the 𝓛-preorder.

Equations

• (x 𝓛 y) = (x ≤𝓛 y ∧ y ≤𝓛 x)

def Semigroup.term_𝓛_ : Lean.TrailingParserDescr

Equations

• Semigroup.term_𝓛_ = Lean.ParserDescr.trailingNode `Semigroup.term_𝓛_ 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " 𝓛 ") (Lean.ParserDescr.cat `term 50))

theorem Semigroup.LEquiv.isEquivalence {S : Type u_1} [Semigroup S] : Equivalence fun (x y : S) => x 𝓛 y

The 𝓛 relation is an equivalence relation.

@[simp]

theorem Semigroup.LEquiv.refl {S : Type u_1} [Semigroup S] (x : S) : x 𝓛 x

@[simp]

theorem Semigroup.LEquiv.symm {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓛 y) : y 𝓛 x

theorem Semigroup.LEquiv.trans {S : Type u_1} [Semigroup S] {x y z : S} (h₁ : x 𝓛 y) (h₂ : y 𝓛 z) : x 𝓛 z

def Semigroup.LEquiv.set {S : Type u_1} [Semigroup S] (x : S) : Set S

The set of all elements 𝓛-related to x.

Equations

• ⟦x⟧𝓛 = {y : S | y 𝓛 x}

def Semigroup.LEquiv.«term⟦_⟧𝓛» : Lean.ParserDescr

Equations

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

@[simp]

theorem Semigroup.LEquiv.set_refl {S : Type u_1} [Semigroup S] (x : S) : x ∈ ⟦x⟧𝓛

def Semigroup.JEquiv {S : Type u_1} [Semigroup S] (x y : S) : Prop

Green's 𝓙 equivalence relation: the symmetric closure of the 𝓙-preorder.

Equations

• (x 𝓙 y) = (x ≤𝓙 y ∧ y ≤𝓙 x)

def Semigroup.term_𝓙_ : Lean.TrailingParserDescr

Equations

• Semigroup.term_𝓙_ = Lean.ParserDescr.trailingNode `Semigroup.term_𝓙_ 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " 𝓙 ") (Lean.ParserDescr.cat `term 50))

theorem Semigroup.JEquiv.isEquivalence {S : Type u_1} [Semigroup S] : Equivalence fun (x y : S) => x 𝓙 y

The 𝓙 relation is an equivalence relation.

@[simp]

theorem Semigroup.JEquiv.refl {S : Type u_1} [Semigroup S] (x : S) : x 𝓙 x

@[simp]

theorem Semigroup.JEquiv.symm {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓙 y) : y 𝓙 x

theorem Semigroup.JEquiv.trans {S : Type u_1} [Semigroup S] {x y z : S} (h₁ : x 𝓙 y) (h₂ : y 𝓙 z) : x 𝓙 z

def Semigroup.JEquiv.set {S : Type u_1} [Semigroup S] (x : S) : Set S

The set of all elements 𝓙-related to x.

Equations

• ⟦x⟧𝓙 = {y : S | y 𝓙 x}

def Semigroup.JEquiv.«term⟦_⟧𝓙» : Lean.ParserDescr

Equations

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

@[simp]

theorem Semigroup.JEquiv.set_refl {S : Type u_1} [Semigroup S] (x : S) : x ∈ ⟦x⟧𝓙

def Semigroup.HEquiv {S : Type u_1} [Semigroup S] (x y : S) : Prop

Green's 𝓗 equivalence relation: the symmetric closure of the 𝓗-preorder.

Equations

• (x 𝓗 y) = (x ≤𝓗 y ∧ y ≤𝓗 x)

def Semigroup.term_𝓗_ : Lean.TrailingParserDescr

Equations

• Semigroup.term_𝓗_ = Lean.ParserDescr.trailingNode `Semigroup.term_𝓗_ 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " 𝓗 ") (Lean.ParserDescr.cat `term 50))

theorem Semigroup.HEquiv.isEquivalence {S : Type u_1} [Semigroup S] : Equivalence fun (x y : S) => x 𝓗 y

The 𝓗 relation is an equivalence relation.

@[simp]

theorem Semigroup.HEquiv.refl {S : Type u_1} [Semigroup S] (x : S) : x 𝓗 x

@[simp]

theorem Semigroup.HEquiv.symm {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓗 y) : y 𝓗 x

theorem Semigroup.HEquiv.trans {S : Type u_1} [Semigroup S] {x y z : S} (h₁ : x 𝓗 y) (h₂ : y 𝓗 z) : x 𝓗 z

def Semigroup.HEquiv.set {S : Type u_1} [Semigroup S] (x : S) : Set S

The set of all elements 𝓗-related to x.

Equations

• ⟦x⟧𝓗 = {y : S | y 𝓗 x}

def Semigroup.HEquiv.«term⟦_⟧𝓗» : Lean.ParserDescr

Equations

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

@[simp]

theorem Semigroup.HEquiv.set_refl {S : Type u_1} [Semigroup S] (x : S) : x ∈ ⟦x⟧𝓗

theorem Semigroup.HEquiv.iff_rEquiv_and_lEquiv {S : Type u_1} [Semigroup S] (x y : S) : x 𝓗 y ↔ x 𝓡 y ∧ x 𝓛 y

The 𝓗 equivalence relation is the intersection of 𝓡 and 𝓛 equivalences.

𝓡 𝓛 Theorems

@[simp]

theorem Semigroup.RPreorder.lmult_compat {S : Type u_1} [Semigroup S] (x y z : S) (h : x ≤𝓡 y) : z * x ≤𝓡 z * y

The 𝓡-preorder is compatible with left multiplication.

@[simp]

theorem Semigroup.REquiv.lmult_compat {S : Type u_1} [Semigroup S] (x y z : S) (h : x 𝓡 y) : z * x 𝓡 z * y

The 𝓡 equivalence is compatible with left multiplication.

@[simp]

theorem Semigroup.LPreorder.rmult_compat {S : Type u_1} [Semigroup S] (x y z : S) (h : x ≤𝓛 y) : x * z ≤𝓛 y * z

The 𝓛-preorder is compatible with right multiplication.

@[simp]

theorem Semigroup.LEquiv.rmult_compat {S : Type u_1} [Semigroup S] (x y z : S) (h : x 𝓛 y) : x * z 𝓛 y * z

The 𝓛 equivalence is compatible with right multiplication.

theorem Semigroup.rEquiv_lEquiv_comm {S : Type u_1} [Semigroup S] (x y : S) : (∃ (z : S), x 𝓡 z ∧ z 𝓛 y) ↔ ∃ (z : S), x 𝓛 z ∧ z 𝓡 y

The 𝓡 and 𝓛 relations commute under composition.

Green's D relation

def Semigroup.DEquiv {S : Type u_1} [Semigroup S] : S → S → Prop

Green's 𝓓 equivalence relation: defined as the composition of 𝓡 and 𝓛.

Equations

• (x 𝓓 y) = ∃ (z : S), x 𝓡 z ∧ z 𝓛 y

def Semigroup.term_𝓓_ : Lean.TrailingParserDescr

Equations

• Semigroup.term_𝓓_ = Lean.ParserDescr.trailingNode `Semigroup.term_𝓓_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " 𝓓 ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem Semigroup.DEquiv.refl {S : Type u_1} [Semigroup S] (x : S) : x 𝓓 x

@[simp]

theorem Semigroup.DEquiv.symm {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓓 y) : y 𝓓 x

theorem Semigroup.DEquiv.closed_under_lEquiv {S : Type u_1} [Semigroup S] {x y z : S} (hd : x 𝓓 y) (hl : y 𝓛 z) : x 𝓓 z

The 𝓓 relation is closed under composition with 𝓛.

theorem Semigroup.DEquiv.closed_under_rEquiv {S : Type u_1} [Semigroup S] {x y z : S} (hd : x 𝓓 y) (hl : y 𝓡 z) : x 𝓓 z

The 𝓓 relation is closed under composition with 𝓡.

theorem Semigroup.DEquiv.trans {S : Type u_1} [Semigroup S] {x y z : S} (h1 : x 𝓓 y) (h2 : y 𝓓 z) : x 𝓓 z

theorem Semigroup.DEquiv.isEquivalence {S : Type u_1} [Semigroup S] : Equivalence fun (x y : S) => x 𝓓 y

The 𝓓 relation is an equivalence relation.

def Semigroup.DEquiv.set {S : Type u_1} [Semigroup S] (x : S) : Set S

Equations

• ⟦x⟧𝓓 = {y : S | y 𝓓 x}

def Semigroup.DEquiv.«term⟦_⟧𝓓» : Lean.ParserDescr

Equations

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

@[simp]

theorem Semigroup.DEquiv.set_refl {S : Type u_1} [Semigroup S] (x : S) : x ∈ ⟦x⟧𝓓

Simp Lemmas

@[simp]

theorem Semigroup.RPreorder.to_jEquiv {S : Type u_1} [Semigroup S] {x y : S} (h : x ≤𝓡 y) : x ≤𝓙 y

x ≤𝓡 y implies x ≤𝓙 y

@[simp]

theorem Semigroup.LPreorder.to_jEquiv {S : Type u_1} [Semigroup S] {x y : S} (h : x ≤𝓛 y) : x ≤𝓙 y

x ≤𝓛 y implies x ≤𝓙 y

@[simp]

theorem Semigroup.REquiv.to_jEquiv {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓡 y) : x 𝓙 y

x 𝓡 y implies x 𝓙 y

@[simp]

theorem Semigroup.LEquiv.to_jEquiv {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓛 y) : x 𝓙 y

x 𝓛 y implies x 𝓙 y

@[simp]

theorem Semigroup.DEquiv.to_jEquiv {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓓 y) : x 𝓙 y

x 𝓓 y implies x 𝓙 y

@[simp]

theorem Semigroup.RPreorder.mul_right_self {S : Type u_1} [Semigroup S] {x y : S} : x * y ≤𝓡 x

x * y is always 𝓡-below x

@[simp]

theorem Semigroup.LPreorder.mul_left_self {S : Type u_1} [Semigroup S] {x y : S} : x * y ≤𝓛 y

x * y is always 𝓛-below y

@[simp]

theorem Semigroup.JPreorder.mul_sandwich_self {S : Type u_1} [Semigroup S] {x y z : S} : x * y * z ≤𝓙 y

x * y * z is always 𝓙-below y

@[simp]

theorem Semigroup.REquiv.of_preorder_mul_right {S : Type u_1} [Semigroup S] {x y : S} (h : x ≤𝓡 x * y) : x 𝓡 x * y

x ≤𝓡 x * y implies x 𝓡 x * y

@[simp]

theorem Semigroup.LEquiv.of_preorder_mul_left {S : Type u_1} [Semigroup S] {x y : S} (h : x ≤𝓛 y * x) : x 𝓛 y * x

x ≤𝓛 y * x implies x 𝓛 y * x

@[simp]

theorem Semigroup.JEquiv.of_preorder_mul_sandwich {S : Type u_1} [Semigroup S] {x y z : S} (h : x ≤𝓙 y * x * z) : x 𝓙 y * x * z

x ≤𝓙 y * x * z implies x 𝓙 y * x * z

@[simp]

theorem Semigroup.REquiv.right_cancel {S : Type u_1} [Semigroup S] {x y z : S} (h : x 𝓡 x * y * z) : x 𝓡 x * y

If x 𝓡 x * y * z, then x 𝓡 x * y.

@[simp]

theorem Semigroup.REquiv.right_extend {S : Type u_1} [Semigroup S] {x y z : S} (h : x 𝓡 x * y * z) : x * y 𝓡 x * y * z

If x 𝓡 x * y * z, then x * y 𝓡 x * y * z.

@[simp]

theorem Semigroup.LEquiv.left_cancel {S : Type u_1} [Semigroup S] {x y z : S} (h : x 𝓛 z * y * x) : x 𝓛 y * x

If x 𝓛 z * y * x, then x 𝓛 y * x.

@[simp]

theorem Semigroup.LEquiv.left_extend {S : Type u_1} [Semigroup S] {x y z : S} (h : x 𝓛 z * y * x) : y * x 𝓛 z * y * x

If x 𝓛 z * y * x, then y * x 𝓛 z * y * x.

le and ge lemmas

@[simp]

theorem Semigroup.REquiv.le {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓡 y) : x ≤𝓡 y

@[simp]

theorem Semigroup.REquiv.ge {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓡 y) : y ≤𝓡 x

@[simp]

theorem Semigroup.LEquiv.le {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓛 y) : x ≤𝓛 y

@[simp]

theorem Semigroup.LEquiv.ge {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓛 y) : y ≤𝓛 x

@[simp]

theorem Semigroup.JEquiv.le {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓙 y) : x ≤𝓙 y

@[simp]

theorem Semigroup.JEquiv.ge {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓙 y) : y ≤𝓙 x

@[simp]

theorem Semigroup.HEquiv.le {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓗 y) : x ≤𝓗 y

@[simp]

theorem Semigroup.HEquiv.ge {S : Type u_1} [Semigroup S] {x y : S} (h : x 𝓗 y) : y ≤𝓗 x