---

Step * of Lemma gcopower_umap_wf

∀s:PosetSig. ∀g:GrpSig. ∀g1:gcopower_sig{i:l}(s;g).  (g1.umap ∈ h:AbGrp ⟶ (|s| ⟶ |g| ⟶ |h|) ⟶ |g1.grp| ⟶ |h|)
BY
{ ModulePiTac 3 ``gcopower_grp gcopower_inj gcopower_umap`` }

---

Latex:

---

Latex:
\mforall{}s:PosetSig.  \mforall{}g:GrpSig.  \mforall{}g1:gcopower\_sig\{i:l\}(s;g).
    (g1.umap  \mmember{}  h:AbGrp  {}\mrightarrow{}  (|s|  {}\mrightarrow{}  |g|  {}\mrightarrow{}  |h|)  {}\mrightarrow{}  |g1.grp|  {}\mrightarrow{}  |h|)


By

---

Latex:
ModulePiTac  3  ``gcopower\_grp  gcopower\_inj  gcopower\_umap``

---

Home Index