---

Step * of Lemma free-group-hom

∀[X:Type]. ∀G:Group{i}. ∀f:X ⟶ |G|.  ∃F:MonHom(free-group(X),G). ∀x:X. ((F free-letter(x)) = (f x) ∈ |G|)
BY
{ (Auto THEN D 0 With ⌜fg-lift(G;f)⌝  THEN Auto) }

1
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. x : X
⊢ (fg-lift(G;f) free-letter(x)) = (f x) ∈ |G|

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}G:Group\{i\}.  \mforall{}f:X  {}\mrightarrow{}  |G|.    \mexists{}F:MonHom(free-group(X),G).  \mforall{}x:X.  ((F  free-letter(x))  =  (f  x))


By

---

Latex:
(Auto  THEN  D  0  With  \mkleeneopen{}fg-lift(G;f)\mkleeneclose{}    THEN  Auto)

---

Home Index