---

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

.....wf..... 
1. S : Type
2. ¬S
3. K : CRng
4. vs : VectorSpace(K)
5. f : S ⟶ Point(vs)
6. h : 0 ⟶ vs
⊢ istype((∀s:S. ((h ⋅) = (f s) ∈ Point(vs))) ∧ (∀y:0 ⟶ vs. ((∀s:S. ((y ⋅) = (f s) ∈ Point(vs))) ⇒ (y = h ∈ 0 ⟶ vs))))
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  S  :  Type
2.  \mneg{}S
3.  K  :  CRng
4.  vs  :  VectorSpace(K)
5.  f  :  S  {}\mrightarrow{}  Point(vs)
6.  h  :  0  {}\mrightarrow{}  vs
\mvdash{}  istype((\mforall{}s:S.  ((h  \mcdot{})  =  (f  s)))  \mwedge{}  (\mforall{}y:0  {}\mrightarrow{}  vs.  ((\mforall{}s:S.  ((y  \mcdot{})  =  (f  s)))  {}\mRightarrow{}  (y  =  h))))


By

---

Latex:
Auto

---

Home Index