---

Step * 1 of Lemma oset_of_ocmon_wf


1. g : OMon
2. IsMonoid(|g|;*;e)
3. Comm(|g|;*)
4. UniformLinorder(|g|;x,y.↑(x ≤b y)) ∧ IsEqFun(|g|;=b)
⊢ g↓oset ∈ LOSet
BY
{ ARepD ["compound"] 
THENM RepeatM MemTypeCD  
THEN Reduce 0 THEN Auto }

1
1. g : OMon
2. Assoc(|g|;*)
3. Ident(|g|;*;e)
4. Comm(|g|;*)
5. UniformlyRefl(|g|;x,y.↑(x ≤b y))
6. UniformlyTrans(|g|;x,y.↑(x ≤b y))
7. UniformlyAntiSym(|g|;x,y.↑(x ≤b y))
8. Connex(|g|;x,y.↑(x ≤b y))
9. ∀[x,y:|g|].  ↑(x ≤b y) supposing ↑(x ≤b y)
10. IsEqFun(|g|;=b)
⊢ UniformPreorder(|g|;a,b.↑(a ≤b b))

---

Latex:

---

Latex:

1.  g  :  OMon
2.  IsMonoid(|g|;*;e)
3.  Comm(|g|;*)
4.  UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))  \mwedge{}  IsEqFun(|g|;=\msubb{})
\mvdash{}  g\mdownarrow{}oset  \mmember{}  LOSet


By

---

Latex:
ARepD  ["compound"] 
THENM  RepeatM  MemTypeCD   
THEN  Reduce  0  THEN  Auto

---

Home Index