---

Step * 1 of Lemma generated-subspace-contains


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))
BY
{ (RenameVar `p' (-1) THEN D 0 With ⌜l_tree_node(1;l_tree_leaf(<v, p>);l_tree_node(0;l_tree_leaf(<v, p>);l_tree_leaf(<v,\000C p>)))⌝  THEN Auto) }

1
1. K : Rng
2. vs : VectorSpace(K)
3. P : Point(vs) ⟶ ℙ
4. v : Point(vs)
5. p : P[v]
⊢ v = vs-tree-val(vs;l_tree_node(1;l_tree_leaf(<v, p>);l_tree_node(0;l_tree_leaf(<v, p>);l_tree_leaf(<v, p>)))) ∈ Point(\000Cvs)

---

Latex:

---

Latex:

1.  K  :  Rng
2.  vs  :  VectorSpace(K)
3.  [P]  :  Point(vs)  {}\mrightarrow{}  \mBbbP{}
4.  v  :  Point(vs)
5.  P[v]
\mvdash{}  \mexists{}t:l\_tree(x:Point(vs)  \mtimes{}  P[x];|K|).  (v  =  vs-tree-val(vs;t))


By

---

Latex:
(RenameVar  `p'  (-1)  THEN  D  0  With  \mkleeneopen{}l\_tree\_node(1;l\_tree\_leaf(<v,  p>);l\_tree\_node(0;l\_tree\_leaf(<v,  p\000C>);l\_tree\_leaf(<v,  p>)))\mkleeneclose{}    THEN  Auto)

---

Home Index