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