---

Step * 1 of Lemma generated-subspace-is-least


1. K : Rng
2. vs : VectorSpace(K)
3. [P] : Point(vs) ⟶ ℙ
4. S : Point(vs) ⟶ ℙ
5. vs-subspace(K;vs;w.S[w])
6. ∀v:Point(vs). (P[v] ⇒ S[v])
7. v : Point(vs)
8. t : l_tree(x:Point(vs) × P[x];|K|)
9. v = vs-tree-val(vs;t) ∈ Point(vs)
⊢ S[vs-tree-val(vs;t)]
BY
{ (Thin (-1)
   THEN MoveToConcl (-1)
   THEN BLemma `l_tree-induction`
   THEN Auto
   THEN Unfold `vs-tree-val` 0
   THEN Reduce 0
   THEN Try (Fold `vs-tree-val` 0)) }

1
1. K : Rng
2. vs : VectorSpace(K)
3. [P] : Point(vs) ⟶ ℙ
4. S : Point(vs) ⟶ ℙ
5. vs-subspace(K;vs;w.S[w])
6. ∀v:Point(vs). (P[v] ⇒ S[v])
7. v : Point(vs)
8. val : x:Point(vs) × P[x]
⊢ S[fst(val)]

2
1. K : Rng
2. vs : VectorSpace(K)
3. [P] : Point(vs) ⟶ ℙ
4. S : Point(vs) ⟶ ℙ
5. vs-subspace(K;vs;w.S[w])
6. ∀v:Point(vs). (P[v] ⇒ S[v])
7. v : Point(vs)
8. val : |K|
9. left_subtree : l_tree(x:Point(vs) × P[x];|K|)
10. right_subtree : l_tree(x:Point(vs) × P[x];|K|)
11. S[vs-tree-val(vs;left_subtree)]
12. S[vs-tree-val(vs;right_subtree)]
⊢ S[val * vs-tree-val(vs;left_subtree) + vs-tree-val(vs;right_subtree)]

---

Latex:

---

Latex:

1.  K  :  Rng
2.  vs  :  VectorSpace(K)
3.  [P]  :  Point(vs)  {}\mrightarrow{}  \mBbbP{}
4.  S  :  Point(vs)  {}\mrightarrow{}  \mBbbP{}
5.  vs-subspace(K;vs;w.S[w])
6.  \mforall{}v:Point(vs).  (P[v]  {}\mRightarrow{}  S[v])
7.  v  :  Point(vs)
8.  t  :  l\_tree(x:Point(vs)  \mtimes{}  P[x];|K|)
9.  v  =  vs-tree-val(vs;t)
\mvdash{}  S[vs-tree-val(vs;t)]


By

---

Latex:
(Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  BLemma  `l\_tree-induction`
  THEN  Auto
  THEN  Unfold  `vs-tree-val`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `vs-tree-val`  0))

---

Home Index