---

Step * 1 2 2 1 1 of Lemma oal_omcp_wf


1. s : LOSet@i'
2. g : OGrp@i'
3. ∀j:|s|. 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. uma\000Cp(h,f)>.inj j)
4. h : AbMon@i'
5. f : |s| ⟶ MonHom(g↓hgrp,h)@i
⊢ umap(h,f) = !v:|oal(s;g↓hgrp)| ⟶ |h|
                (IsMonHom{oal_mon(s;g↓hgrp),h}(v) ∧ (∀j:|s|. ((f j) = (v o (λv.inj(j,v))) ∈ (|(g↓hgrp)| ⟶ |h|))))
BY
{ (((BLemma `oal_umap_char_a`) THEN Auto) THEN BLemma `omon_inc` THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  \mforall{}j:|s|.  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.\000C  inj(k,v),  \mlambda{}h,f.  umap(h,f)>.inj  j)
4.  h  :  AbMon@i'
5.  f  :  |s|  {}\mrightarrow{}  MonHom(g\mdownarrow{}hgrp,h)@i
\mvdash{}  umap(h,f)  =  !v:|oal(s;g\mdownarrow{}hgrp)|  {}\mrightarrow{}  |h|
                                (IsMonHom\{oal\_mon(s;g\mdownarrow{}hgrp),h\}(v)  \mwedge{}  (\mforall{}j:|s|.  ((f  j)  =  (v  o  (\mlambda{}v.inj(j,v))))))


By

---

Latex:
(((BLemma  `oal\_umap\_char\_a`)  THEN  Auto)  THEN  BLemma  `omon\_inc`  THEN  Auto)

---

Home Index