---

Step * 1 1 1 1 1 1 1 1 of Lemma no-retraction-case-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)
BY
{ (RepUR ``req-vec`` -3
   THEN (RWO "req-rat2real" (-3) THENA Auto)
   THEN Unfold `rational-cube` 0
   THEN (FunExt THENW Auto)) }

1
1. k : ℕ
2. v2 : ℚCube(k)
3. v3 : ℚCube(k)
4. ∀i:ℕk. ((fst((v2 i))) = (fst((v3 i))) ∈ ℚ)
5. ∀i:ℕk. ((fst((v2 i))) = (snd((v2 i))) ∈ ℚ)
6. ∀i:ℕk. ((fst((v3 i))) = (snd((v3 i))) ∈ ℚ)
7. x : ℕk
⊢ (v2 x) = (v3 x) ∈ ℚInterval

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  v2  :  \mBbbQ{}Cube(k)
3.  v3  :  \mBbbQ{}Cube(k)
4.  req-vec(k;\mlambda{}j.rat2real(fst((v2  j)));\mlambda{}j.rat2real(fst((v3  j))))
5.  \mforall{}i:\mBbbN{}k.  ((fst((v2  i)))  =  (snd((v2  i))))
6.  \mforall{}i:\mBbbN{}k.  ((fst((v3  i)))  =  (snd((v3  i))))
\mvdash{}  v2  =  v3


By

---

Latex:
(RepUR  ``req-vec``  -3
  THEN  (RWO  "req-rat2real"  (-3)  THENA  Auto)
  THEN  Unfold  `rational-cube`  0
  THEN  (FunExt  THENW  Auto))

---

Home Index