---

Step * 3 of Lemma fg-lift_wf

.....wf..... 
1. X : Type
2. G : Group{i}@i'
3. f : X ⟶ |G|@i
4. F : MonHom(free-group(X),G)
⊢ ∀x:X. ((F free-letter(x)) = (f x) ∈ |G|) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  X  :  Type
2.  G  :  Group\{i\}@i'
3.  f  :  X  {}\mrightarrow{}  |G|@i
4.  F  :  MonHom(free-group(X),G)
\mvdash{}  \mforall{}x:X.  ((F  free-letter(x))  =  (f  x))  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index