---

Step * of Lemma vs-lift-inc

∀[S:Type]. ∀[K:Rng]. ∀[s:S]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].  (vs-lift(vs;f;<s>) = (f s) ∈ Point(vs))
BY
{ (Auto
   THEN RepUR ``vs-lift free-vs-inc vs-bag-add`` 0
   THEN RWO "bag-summation-single" 0
   THEN Auto
   THEN RepeatFor 2 ((Try (D 0) THEN Reduce 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:Rng].  \mforall{}[s:S].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[f:S  {}\mrightarrow{}  Point(vs)].    (vs-lift(vs;f;<s>)  =  (f  s))


By

---

Latex:
(Auto
  THEN  RepUR  ``vs-lift  free-vs-inc  vs-bag-add``  0
  THEN  RWO  "bag-summation-single"  0
  THEN  Auto
  THEN  RepeatFor  2  ((Try  (D  0)  THEN  Reduce  0  THEN  Auto)))

---

Home Index