---

Step * 1 2 1 of Lemma oal_omcp_wf


1. s : LOSet@i'
2. g : OGrp@i'
3. j : |s|@i
⊢ IsMonHom{g↓hgrp,<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon}(<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.i\000Cnj j)
BY
{ Force `6` (Reduce 0)⋅ }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. j : |s|@i
⊢ IsMonHom{g↓hgrp,oal_hgp(s;g)}(λv.inj(j,v))

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  j  :  |s|@i
\mvdash{}  IsMonHom\{g\mdownarrow{}hgrp,<oal\_hgp(s;g),  \mlambda{}k,v.  inj(k,v),  \mlambda{}h,f.  umap(h,f)>.mon\}(<oal\_hgp(s;g),  \mlambda{}k,v.  inj(k,v)\000C,  \mlambda{}h,f.  umap(h,f)>.inj  j)


By

---

Latex:
Force  `6`  (Reduce  0)\mcdot{}

---

Home Index