---

Step * of Lemma vs-lift_wf-vs-map

∀[S:Type]. ∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].  (λx.vs-lift(vs;f;x) ∈ free-vs(K;S) ⟶ vs)
BY
{ (Auto THEN MemTypeCD THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:CRng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[f:S  {}\mrightarrow{}  Point(vs)].
    (\mlambda{}x.vs-lift(vs;f;x)  \mmember{}  free-vs(K;S)  {}\mrightarrow{}  vs)


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index