---

Step * 1 1 of Lemma free-vs-unique


1. S : Type
2. K : CRng
3. V : VectorSpace(K)
4. i : S ⟶ Point(V)
5. ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:V ⟶ vs. ∀s:S. ((h (i s)) = (f s) ∈ Point(vs))
6. ∃!h:free-vs(K;S) ⟶ V. ∀s:S. ((h <s>) = (i s) ∈ Point(V))
⊢ V ≅ free-vs(K;S)
BY
{ ((InstHyp [⌜free-vs(K;S)⌝;⌜λs.<s>⌝] (-2)⋅ THENA Auto)
   THEN Reduce -1
   THEN RepeatFor 2 (D -1)
   THEN RenameVar `f' (-3)
   THEN Thin (-1)
   THEN (D -3 THEN ExRepD)
   THEN Thin (-3)) }

1
1. S : Type
2. K : CRng
3. V : VectorSpace(K)
4. i : S ⟶ Point(V)
5. ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:V ⟶ vs. ∀s:S. ((h (i s)) = (f s) ∈ Point(vs))
6. h : free-vs(K;S) ⟶ V
7. ∀s:S. ((h <s>) = (i s) ∈ Point(V))
8. f : V ⟶ free-vs(K;S)
9. ∀s:S. ((f (i s)) = <s> ∈ Point(free-vs(K;S)))
⊢ V ≅ free-vs(K;S)

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  V  :  VectorSpace(K)
4.  i  :  S  {}\mrightarrow{}  Point(V)
5.  \mforall{}vs:VectorSpace(K).  \mforall{}f:S  {}\mrightarrow{}  Point(vs).    \mexists{}!h:V  {}\mrightarrow{}  vs.  \mforall{}s:S.  ((h  (i  s))  =  (f  s))
6.  \mexists{}!h:free-vs(K;S)  {}\mrightarrow{}  V.  \mforall{}s:S.  ((h  <s>)  =  (i  s))
\mvdash{}  V  \mcong{}  free-vs(K;S)


By

---

Latex:
((InstHyp  [\mkleeneopen{}free-vs(K;S)\mkleeneclose{};\mkleeneopen{}\mlambda{}s.<s>\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  RepeatFor  2  (D  -1)
  THEN  RenameVar  `f'  (-3)
  THEN  Thin  (-1)
  THEN  (D  -3  THEN  ExRepD)
  THEN  Thin  (-3))

---

Home Index