---

Step * 1 of Lemma free_abmon_umap_properties_1


1. S : DSet
2. M : FAbMon(S)
3. N : AbMon
4. p : |S| ⟶ |N|
⊢ ((M.umap N p) o M.inj) = p ∈ (|S| ⟶ |N|)
BY
{ D 2 THEN D 3 
THEN AbReduce 0 }

1
1. S : DSet
2. mon : AbMon
3. inj : |S| ⟶ |mon|
4. M2 : mon':AbMon ⟶ f':(|S| ⟶ |mon'|) ⟶ {!g:MonHom(mon,mon') | (g o inj) = f' ∈ (|S| ⟶ |mon'|)}
5. N : AbMon
6. p : |S| ⟶ |N|
⊢ ((M2 N p) o inj) = p ∈ (|S| ⟶ |N|)

---

Latex:

---

Latex:

1.  S  :  DSet
2.  M  :  FAbMon(S)
3.  N  :  AbMon
4.  p  :  |S|  {}\mrightarrow{}  |N|
\mvdash{}  ((M.umap  N  p)  o  M.inj)  =  p


By

---

Latex:
D  2  THEN  D  3 
THEN  AbReduce  0

---

Home Index