---

Step * 1 2 1 1 1 1 2 of Lemma vs-lift-unique


1. S : Type
2. K : CRng
3. vs : VectorSpace(K)
4. f : S ⟶ Point(vs)
5. h : Point(free-vs(K;S)) ⟶ Point(vs)
6. ∀u,v:Point(free-vs(K;S)).  ((h u + v) = h u + h v ∈ Point(vs))
7. ∀a:|K|. ∀u:Point(free-vs(K;S)).  ((h a * u) = a * h u ∈ Point(vs))
8. ∀s:S. ((h <s>) = (f s) ∈ Point(vs))
9. (h []) = 0 ∈ Point(vs)
10. u : |K| × S
11. v : (|K| × S) List
12. (h v) = vs-lift(vs;f;v) ∈ Point(vs)
⊢ (h [u / v]) = vs-lift(vs;f;[u / v]) ∈ Point(vs)
BY
{ (Subst' [u / v] ~ {u} + v 0 THENA (RepUR ``bag-append single-bag`` 0 THEN Auto)) }

1
1. S : Type
2. K : CRng
3. vs : VectorSpace(K)
4. f : S ⟶ Point(vs)
5. h : Point(free-vs(K;S)) ⟶ Point(vs)
6. ∀u,v:Point(free-vs(K;S)).  ((h u + v) = h u + h v ∈ Point(vs))
7. ∀a:|K|. ∀u:Point(free-vs(K;S)).  ((h a * u) = a * h u ∈ Point(vs))
8. ∀s:S. ((h <s>) = (f s) ∈ Point(vs))
9. (h []) = 0 ∈ Point(vs)
10. u : |K| × S
11. v : (|K| × S) List
12. (h v) = vs-lift(vs;f;v) ∈ Point(vs)
⊢ (h ({u} + v)) = vs-lift(vs;f;{u} + v) ∈ Point(vs)

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  vs  :  VectorSpace(K)
4.  f  :  S  {}\mrightarrow{}  Point(vs)
5.  h  :  Point(free-vs(K;S))  {}\mrightarrow{}  Point(vs)
6.  \mforall{}u,v:Point(free-vs(K;S)).    ((h  u  +  v)  =  h  u  +  h  v)
7.  \mforall{}a:|K|.  \mforall{}u:Point(free-vs(K;S)).    ((h  a  *  u)  =  a  *  h  u)
8.  \mforall{}s:S.  ((h  <s>)  =  (f  s))
9.  (h  [])  =  0
10.  u  :  |K|  \mtimes{}  S
11.  v  :  (|K|  \mtimes{}  S)  List
12.  (h  v)  =  vs-lift(vs;f;v)
\mvdash{}  (h  [u  /  v])  =  vs-lift(vs;f;[u  /  v])


By

---

Latex:
(Subst'  [u  /  v]  \msim{}  \{u\}  +  v  0  THENA  (RepUR  ``bag-append  single-bag``  0  THEN  Auto))

---

Home Index