---

Step * of Lemma gcopower_inj_wf

∀s:PosetSig. ∀g:GrpSig. ∀g1:gcopower_sig{i:l}(s;g).  (g1.inj ∈ |s| ⟶ |g| ⟶ |g1.grp|)
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.inj  \mmember{}  |s|  {}\mrightarrow{}  |g|  {}\mrightarrow{}  |g1.grp|)


By

---

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

---

Home Index