---

Step * of Lemma subtype-vs-quotient

∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].  Point(vs) ⊆r Point(vs//z.P[z]) supposing vs-subspace(K;vs;z.P[z])
BY
{ (Auto THEN RepUR ``vs-quotient mk-vs vs-point`` 0 THEN Fold `vs-point` 0 THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[P:Point(vs)  {}\mrightarrow{}  \mBbbP{}].
    Point(vs)  \msubseteq{}r  Point(vs//z.P[z])  supposing  vs-subspace(K;vs;z.P[z])


By

---

Latex:
(Auto  THEN  RepUR  ``vs-quotient  mk-vs  vs-point``  0  THEN  Fold  `vs-point`  0  THEN  EAuto  1)

---

Home Index