---

Step * 1 1 1 1 1 1 of Lemma no-retraction-case-1


1. k : ℕ
2. x : ℝ^k
3. y : ℝ^k
4. v : ℚCube(k) List
5. no_repeats(ℚCube(k);v)
6. (∀c,d∈v.  Compatible(c;d))
7. (∀c∈v.dim(c) = 0 ∈ ℤ)
8. v@0 : ℕ||v||
9. v1 : ℕ||v||
10. req-vec(k;x;y)
11. req-vec(k;x;λj.rat2real(fst((v[v@0] j))))
12. req-vec(k;y;λj.rat2real(fst((v[v1] j))))
13. ¬(v@0 = v1 ∈ ℤ)
⊢ False
BY
{ ((D 5 With ⌜v@0⌝  THENA Auto)
   THEN InstHyp [⌜v1⌝] (-1)⋅
   THEN Auto
   THEN D -1
   THEN (Assert req-vec(k;λj.rat2real(fst((v[v@0] j)));λj.rat2real(fst((v[v1] j)))) BY
               (RelRST THEN Auto))) }

1
1. k : ℕ
2. x : ℝ^k
3. y : ℝ^k
4. v : ℚCube(k) List
5. (∀c,d∈v.  Compatible(c;d))
6. (∀c∈v.dim(c) = 0 ∈ ℤ)
7. v@0 : ℕ||v||
8. v1 : ℕ||v||
9. req-vec(k;x;y)
10. req-vec(k;x;λj.rat2real(fst((v[v@0] j))))
11. req-vec(k;y;λj.rat2real(fst((v[v1] j))))
12. ¬(v@0 = v1 ∈ ℤ)
13. ∀[j:ℕ]. (¬(v[v@0] = v[j] ∈ ℚCube(k))) supposing ((¬(v@0 = j ∈ ℕ)) and j < ||v|| and v@0 < ||v||)
14. req-vec(k;λj.rat2real(fst((v[v@0] j)));λj.rat2real(fst((v[v1] j))))
⊢ v[v@0] = v[v1] ∈ ℚCube(k)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  x  :  \mBbbR{}\^{}k
3.  y  :  \mBbbR{}\^{}k
4.  v  :  \mBbbQ{}Cube(k)  List
5.  no\_repeats(\mBbbQ{}Cube(k);v)
6.  (\mforall{}c,d\mmember{}v.    Compatible(c;d))
7.  (\mforall{}c\mmember{}v.dim(c)  =  0)
8.  v@0  :  \mBbbN{}||v||
9.  v1  :  \mBbbN{}||v||
10.  req-vec(k;x;y)
11.  req-vec(k;x;\mlambda{}j.rat2real(fst((v[v@0]  j))))
12.  req-vec(k;y;\mlambda{}j.rat2real(fst((v[v1]  j))))
13.  \mneg{}(v@0  =  v1)
\mvdash{}  False


By

---

Latex:
((D  5  With  \mkleeneopen{}v@0\mkleeneclose{}    THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}v1\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto
  THEN  D  -1
  THEN  (Assert  req-vec(k;\mlambda{}j.rat2real(fst((v[v@0]  j)));\mlambda{}j.rat2real(fst((v[v1]  j))))  BY
                          (RelRST  THEN  Auto)))

---

Home Index