---

Step * 2 1 of Lemma oal_hgp_wf2


1. s : LOSet@i'
2. g : OGrp@i'
3. (g↓hgrp ∈ AbDMon) ∧ (g ∈ AbDMon)
⊢ IsMonHomInj(oal_hgp(s;g);oal_grp(s;g);λz.z)
∧ RelsIso(|oal_hgp(s;g)|;|oal_grp(s;g)|;x,y.↑(x =b y);x,y.↑(x =b y);λz.z)
∧ RelsIso(|oal_hgp(s;g)|;|oal_grp(s;g)|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);λz.z)
BY
{ ((Force `5` (Reduce 0) THENM GenRepD) THENA Auto) }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. g↓hgrp ∈ AbDMon
4. g ∈ AbDMon
⊢ IsMonHomInj(oal_hgp(s;g);oal_grp(s;g);λz.z)

2
1. s : LOSet@i'
2. g : OGrp@i'
3. g↓hgrp ∈ AbDMon
4. g ∈ AbDMon
⊢ RelsIso(|oal(s;g↓hgrp)|;|oal(s;g)|;x,y.↑(x (=b) y);x,y.↑(x (=b) y);λz.z)

3
1. s : LOSet@i'
2. g : OGrp@i'
3. g↓hgrp ∈ AbDMon
4. g ∈ AbDMon
⊢ RelsIso(|oal(s;g↓hgrp)|;|oal(s;g)|;x,y.↑x ≤≤b y;x,y.↑x ≤≤b y;λz.z)

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  (g\mdownarrow{}hgrp  \mmember{}  AbDMon)  \mwedge{}  (g  \mmember{}  AbDMon)
\mvdash{}  IsMonHomInj(oal\_hgp(s;g);oal\_grp(s;g);\mlambda{}z.z)
\mwedge{}  RelsIso(|oal\_hgp(s;g)|;|oal\_grp(s;g)|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);\mlambda{}z.z)
\mwedge{}  RelsIso(|oal\_hgp(s;g)|;|oal\_grp(s;g)|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}z.z)


By

---

Latex:
((Force  `5`  (Reduce  0)  THENM  GenRepD)  THENA  Auto)

---

Home Index