---

Step * of Lemma free-vs-unique

∀S:Type. ∀K:CRng. ∀V:VectorSpace(K).
  (∃i:S ⟶ Point(V). ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:V ⟶ vs. ∀s:S. ((h (i s)) = (f s) ∈ Point(vs))
  ⇐⇒ V ≅ free-vs(K;S))
BY
{ Auto }

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

2
1. S : Type
2. K : CRng
3. V : VectorSpace(K)
4. V ≅ 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))

---

Latex:

---

Latex:
\mforall{}S:Type.  \mforall{}K:CRng.  \mforall{}V:VectorSpace(K).
    (\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))
    \mLeftarrow{}{}\mRightarrow{}  V  \mcong{}  free-vs(K;S))


By

---

Latex:
Auto

---

Home Index