---

Step * 1 1 2 1 1 of Lemma 0-dim-complex-polyhedron

.....assertion..... 
1. k : ℕ
2. K : 0-dim-complex
3. x : |K|
4. u : ℕk ⟶ ℚ
5. v : (ℕk ⟶ ℚ) List
6. no_repeats(ℕk ⟶ ℚ;v)
7. ¬(u ∈ v)
8. Stable{∃i:ℕ||v||. req-vec(k;x;λj.rat2real(v[i] j))}
⊢ ∀i:ℕ||v||. λj.rat2real(u j) ≠ λj.rat2real(v[i] j)
BY
{ ((D 0 THENA Auto)
   THEN (Assert ⌜¬(u = v[i] ∈ (ℕk ⟶ ℚ))⌝⋅ THENA (ParallelOp -3 THEN D 0 With ⌜i⌝  THEN Auto))
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜v[i] = a ∈ (ℕk ⟶ ℚ)⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. k : ℕ
2. u : ℕk ⟶ ℚ
3. a : ℕk ⟶ ℚ
⊢ (¬(u = a ∈ (ℕk ⟶ ℚ))) ⇒ λj.rat2real(u j) ≠ λj.rat2real(a j)

---

Latex:

---

Latex:
.....assertion..... 
1.  k  :  \mBbbN{}
2.  K  :  0-dim-complex
3.  x  :  |K|
4.  u  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}
5.  v  :  (\mBbbN{}k  {}\mrightarrow{}  \mBbbQ{})  List
6.  no\_repeats(\mBbbN{}k  {}\mrightarrow{}  \mBbbQ{};v)
7.  \mneg{}(u  \mmember{}  v)
8.  Stable\{\mexists{}i:\mBbbN{}||v||.  req-vec(k;x;\mlambda{}j.rat2real(v[i]  j))\}
\mvdash{}  \mforall{}i:\mBbbN{}||v||.  \mlambda{}j.rat2real(u  j)  \mneq{}  \mlambda{}j.rat2real(v[i]  j)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mneg{}(u  =  v[i])\mkleeneclose{}\mcdot{}  THENA  (ParallelOp  -3  THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{}    THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}v[i]  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index