---

Step * of Lemma generated-subspace-contains

∀K:Rng. ∀vs:VectorSpace(K).  ∀[P:Point(vs) ⟶ ℙ]. ∀v:Point(vs). (P[v] ⇒ (Subspace(x.P[x]) v))
BY
{ (Auto THEN RepUR ``generated-subspace`` 0 THEN OrRight THEN Auto) }

1
1. K : Rng
2. vs : VectorSpace(K)
3. [P] : Point(vs) ⟶ ℙ
4. v : Point(vs)
5. P[v]
⊢ ∃t:l_tree(x:Point(vs) × P[x];|K|). (v = vs-tree-val(vs;t) ∈ Point(vs))

---

Latex:

---

Latex:
\mforall{}K:Rng.  \mforall{}vs:VectorSpace(K).    \mforall{}[P:Point(vs)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}v:Point(vs).  (P[v]  {}\mRightarrow{}  (Subspace(x.P[x])  v))


By

---

Latex:
(Auto  THEN  RepUR  ``generated-subspace``  0  THEN  OrRight  THEN  Auto)

---

Home Index