---

Step * 1 of Lemma oal_grp_wf1


1. s : LOSet
2. g : OGrp
3. g ∈ AbDGrp
4. g ∈ AbDMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
⊢ oal_grp(s;g) ∈ OMon
BY
{ (MemTypeCD THEN Auto) }

1
1. s : LOSet
2. g : OGrp
3. g ∈ AbDGrp
4. g ∈ AbDMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
6. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
⊢ =b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|oal_grp(s;g)| ⟶ |oal_grp(s;g)| ⟶ 𝔹)

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  OGrp
3.  g  \mmember{}  AbDGrp
4.  g  \mmember{}  AbDMon
5.  UniformLinorder(|oal\_grp(s;g)|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
\mvdash{}  oal\_grp(s;g)  \mmember{}  OMon


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index