---

Step * of Lemma fg-lift_wf

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

1
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
⊢ fg-lift(G;f) ∈ MonHom(free-group(X),G)

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  MemTypeCD)

---

Home Index