---

Step * of Lemma free-vs-property

∀[S:Type]. ∀K:CRng. ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:free-vs(K;S) ⟶ vs. ∀s:S. ((h <s>) = (f s) ∈ Point(vs))
BY
{ (InstLemma `vs-lift_wf-vs-map` []
   THEN RepeatFor 4 (ParallelLast')
   THEN InstLemma `vs-lift-unique` [⌜S⌝;⌜K⌝;⌜vs⌝;⌜f⌝]⋅
   THEN Auto
   THEN D 0 With ⌜λx.vs-lift(vs;f;x)⌝ 
   THEN Auto
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[S:Type]
    \mforall{}K:CRng.  \mforall{}vs:VectorSpace(K).  \mforall{}f:S  {}\mrightarrow{}  Point(vs).    \mexists{}!h:free-vs(K;S)  {}\mrightarrow{}  vs.  \mforall{}s:S.  ((h  <s>)  =  (f  s))


By

---

Latex:
(InstLemma  `vs-lift\_wf-vs-map`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  InstLemma  `vs-lift-unique`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}vs\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0  With  \mkleeneopen{}\mlambda{}x.vs-lift(vs;f;x)\mkleeneclose{} 
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto)

---

Home Index