---

Step * 1 of Lemma free-vs-dim-1


1. S : Type
2. s : S
3. K : CRng
4. ∀x,y:S.  (x = y ∈ S)
5. vs : VectorSpace(K)
6. f : S ⟶ Point(vs)
⊢ ∃!h:one-dim-vs(K) ⟶ vs. ∀s:S. ((h 1) = (f s) ∈ Point(vs))
BY
{ Assert ⌜∃!h:one-dim-vs(K) ⟶ vs. ((h 1) = (f s) ∈ Point(vs))⌝⋅ }

1
.....assertion..... 
1. S : Type
2. s : S
3. K : CRng
4. ∀x,y:S.  (x = y ∈ S)
5. vs : VectorSpace(K)
6. f : S ⟶ Point(vs)
⊢ ∃!h:one-dim-vs(K) ⟶ vs. ((h 1) = (f s) ∈ Point(vs))

2
1. S : Type
2. s : S
3. K : CRng
4. ∀x,y:S.  (x = y ∈ S)
5. vs : VectorSpace(K)
6. f : S ⟶ Point(vs)
7. ∃!h:one-dim-vs(K) ⟶ vs. ((h 1) = (f s) ∈ Point(vs))
⊢ ∃!h:one-dim-vs(K) ⟶ vs. ∀s:S. ((h 1) = (f s) ∈ Point(vs))

---

Latex:

---

Latex:

1.  S  :  Type
2.  s  :  S
3.  K  :  CRng
4.  \mforall{}x,y:S.    (x  =  y)
5.  vs  :  VectorSpace(K)
6.  f  :  S  {}\mrightarrow{}  Point(vs)
\mvdash{}  \mexists{}!h:one-dim-vs(K)  {}\mrightarrow{}  vs.  \mforall{}s:S.  ((h  1)  =  (f  s))


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}!h:one-dim-vs(K)  {}\mrightarrow{}  vs.  ((h  1)  =  (f  s))\mkleeneclose{}\mcdot{}

---

Home Index