---

Step * 1 of Lemma vs-lift-unique


1. S : Type
2. K : CRng
3. vs : VectorSpace(K)
4. f : S ⟶ Point(vs)
5. h : free-vs(K;S) ⟶ vs
6. ∀s:S. ((h <s>) = (f s) ∈ Point(vs))
⊢ h = (λx.vs-lift(vs;f;x)) ∈ free-vs(K;S) ⟶ vs
BY
{ (DVar `h' THEN EqTypeCD THEN Auto THEN (FunExt THENA Auto) THEN Reduce 0 THEN Assert ⌜(h []) = 0 ∈ Point(vs)⌝⋅) }

1
.....assertion..... 
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. x : Point(free-vs(K;S))
⊢ (h []) = 0 ∈ Point(vs)

2
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. x : Point(free-vs(K;S))
10. (h []) = 0 ∈ Point(vs)
⊢ (h x) = vs-lift(vs;f;x) ∈ Point(vs)

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  vs  :  VectorSpace(K)
4.  f  :  S  {}\mrightarrow{}  Point(vs)
5.  h  :  free-vs(K;S)  {}\mrightarrow{}  vs
6.  \mforall{}s:S.  ((h  <s>)  =  (f  s))
\mvdash{}  h  =  (\mlambda{}x.vs-lift(vs;f;x))


By

---

Latex:
(DVar  `h'  THEN  EqTypeCD  THEN  Auto  THEN  (FunExt  THENA  Auto)  THEN  Reduce  0  THEN  Assert  \mkleeneopen{}(h  [])  =  0\mkleeneclose{}\mcdot{})

---

Home Index