---

Step * 1 of Lemma all-vs-quotient-of-free


1. K : CRng
2. V : VectorSpace(K)
⊢ ∃f:free-vs(K;Point(V)) ⟶ V. Surj(Point(free-vs(K;Point(V)));Point(V);f)
BY
{ ((InstLemma `free-vs-property` [⌜Point(V)⌝;⌜K⌝;⌜V⌝;⌜λx.x⌝]⋅ THENA Auto) THEN D -1 THEN D 0 With ⌜h⌝  THEN Auto) }

1
1. K : CRng
2. V : VectorSpace(K)
3. h : free-vs(K;Point(V)) ⟶ V
4. ∀s:Point(V). ((h <s>) = ((λx.x) s) ∈ Point(V))
5. ∀y:free-vs(K;Point(V)) ⟶ V. ((∀s:Point(V). ((y <s>) = ((λx.x) s) ∈ Point(V))) ⇒ (y = h ∈ free-vs(K;Point(V)) ⟶ V))
⊢ Surj(Point(free-vs(K;Point(V)));Point(V);h)

---

Latex:

---

Latex:

1.  K  :  CRng
2.  V  :  VectorSpace(K)
\mvdash{}  \mexists{}f:free-vs(K;Point(V))  {}\mrightarrow{}  V.  Surj(Point(free-vs(K;Point(V)));Point(V);f)


By

---

Latex:
((InstLemma  `free-vs-property`  [\mkleeneopen{}Point(V)\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  D  0  With  \mkleeneopen{}h\mkleeneclose{} 
  THEN  Auto)

---

Home Index