---

Step * 2 1 of Lemma free-vs-unique


1. S : Type
2. K : CRng
3. V : VectorSpace(K)
4. f : V ⟶ free-vs(K;S)
5. g : free-vs(K;S) ⟶ V
6. ∀a:Point(V). ((g (f a)) = a ∈ Point(V))
7. ∀b:Point(free-vs(K;S)). ((f (g b)) = b ∈ Point(free-vs(K;S)))
⊢ ∃i:S ⟶ Point(V). ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:V ⟶ vs. ∀s:S. ((h (i s)) = (f s) ∈ Point(vs))
BY
{ ((D 0 With ⌜λs.(g <s>)⌝  THEN Auto) THEN Reduce 0) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((D  0  With  \mkleeneopen{}\mlambda{}s.(g  <s>)\mkleeneclose{}    THEN  Auto)  THEN  Reduce  0)

---

Home Index