---

Step * of Lemma fabgrp_umap_wf

∀s:DSet. ∀f:fabgrp_sig{i:l}(s).  (f.umap ∈ grp':AbGrp ⟶ (|s| ⟶ |grp'|) ⟶ |f.grp| ⟶ |grp'|)
BY
{ ModulePiTac 3 ``fabgrp_grp fabgrp_inj fabgrp_umap`` }

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}f:fabgrp\_sig\{i:l\}(s).    (f.umap  \mmember{}  grp':AbGrp  {}\mrightarrow{}  (|s|  {}\mrightarrow{}  |grp'|)  {}\mrightarrow{}  |f.grp|  {}\mrightarrow{}  |grp'|)


By

---

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

---

Home Index