---

Step * of Lemma vs-lift_wf-relative

∀[S,T:Type].
  ∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[f:S ⟶ Point(vs)].
    λx.vs-lift(vs;f;x) ∈ relative-free-vs(K;S;T) ⟶ vs supposing ∀t:T. (↓(f t) = 0 ∈ Point(vs)) 
  supposing strong-subtype(T;S)
BY
{ (Intros THEN Unhide) }

1
1. S : Type
2. T : Type
3. strong-subtype(T;S)
4. K : CRng
5. vs : VectorSpace(K)
6. f : S ⟶ Point(vs)
7. ∀t:T. (↓(f t) = 0 ∈ Point(vs))
⊢ λx.vs-lift(vs;f;x) ∈ relative-free-vs(K;S;T) ⟶ vs

---

Latex:

---

Latex:
\mforall{}[S,T:Type].
    \mforall{}[K:CRng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[f:S  {}\mrightarrow{}  Point(vs)].
        \mlambda{}x.vs-lift(vs;f;x)  \mmember{}  relative-free-vs(K;S;T)  {}\mrightarrow{}  vs  supposing  \mforall{}t:T.  (\mdownarrow{}(f  t)  =  0) 
    supposing  strong-subtype(T;S)


By

---

Latex:
(Intros  THEN  Unhide)

---

Home Index