---

Step * of Lemma free_abmon_umap_properties

∀S:DSet. ∀M:FAbMon(S). ∀N:AbMon. ∀p:|S| ⟶ |N|.
  ((((M.umap N p) o M.inj) = p ∈ (|S| ⟶ |N|))
  ∧ (∀f:MonHom(M.mon,N). (((f o M.inj) = p ∈ (|S| ⟶ |N|)) ⇒ (f = (M.umap N p) ∈ (|M.mon| ⟶ |N|)))))
BY
{ ((UnivCD) THENA Auto) }

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|))
∧ (∀f:MonHom(M.mon,N). (((f o M.inj) = p ∈ (|S| ⟶ |N|)) ⇒ (f = (M.umap N p) ∈ (|M.mon| ⟶ |N|))))

---

Latex:

---

Latex:
\mforall{}S:DSet.  \mforall{}M:FAbMon(S).  \mforall{}N:AbMon.  \mforall{}p:|S|  {}\mrightarrow{}  |N|.
    ((((M.umap  N  p)  o  M.inj)  =  p)  \mwedge{}  (\mforall{}f:MonHom(M.mon,N).  (((f  o  M.inj)  =  p)  {}\mRightarrow{}  (f  =  (M.umap  N  p)))))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index