---

Step * 1 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. (∀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)
BY
{ ((DupHyp 6 THEN (D -1 With ⌜v@0⌝  THENA Auto))
   THEN DupHyp 6
   THEN (D -1 With ⌜v1⌝  THENA Auto)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜v[v@0]⌝;⌜v[v1]⌝]⋅
   THEN All Thin
   THEN RWO "rat-cube-dimension-zero" 0
   THEN Auto) }

1
1. k : ℕ
2. v2 : ℚCube(k)
3. v3 : ℚCube(k)
4. req-vec(k;λj.rat2real(fst((v2 j)));λj.rat2real(fst((v3 j))))
5. ∀i:ℕk. ((fst((v2 i))) = (snd((v2 i))) ∈ ℚ)
6. ∀i:ℕk. ((fst((v3 i))) = (snd((v3 i))) ∈ ℚ)
⊢ v2 = v3 ∈ ℚCube(k)

---

Latex:

---

Latex:

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


By

---

Latex:
((DupHyp  6  THEN  (D  -1  With  \mkleeneopen{}v@0\mkleeneclose{}    THENA  Auto))
  THEN  DupHyp  6
  THEN  (D  -1  With  \mkleeneopen{}v1\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}v[v@0]\mkleeneclose{};\mkleeneopen{}v[v1]\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  RWO  "rat-cube-dimension-zero"  0
  THEN  Auto)

---

Home Index