---

Step * of Lemma intersecting-0-dim-cubes

∀k:ℕ. ∀b:ℚCube(k). ∀q:ℝ^k. ∀c:ℚCube(k).
  ((in-rat-cube(k;q;c) ∧ in-rat-cube(k;q;b) ∧ (dim(c) = 0 ∈ ℤ) ∧ (dim(b) = 0 ∈ ℤ)) ⇒ (c = b ∈ ℚCube(k)))
BY
{ (Auto
   THEN (All (RWO "in-0-dim-cube") THENA Auto)
   THEN (Assert req-vec(k;λj.rat2real(fst((c j)));λj.rat2real(fst((b j)))) BY
               (RelRST THEN Auto))
   THEN RepUR ``req-vec`` -1
   THEN (RWO "req-rat2real" (-1) THENA Auto)
   THEN (All (RWO "rat-cube-dimension-zero") THENA Auto)
   THEN Unfold `rational-cube` 0
   THEN FunExt
   THEN Auto) }

1
1. k : ℕ
2. b : ℚCube(k)
3. q : ℝ^k
4. c : ℚCube(k)
5. req-vec(k;q;λj.rat2real(fst((c j))))
6. req-vec(k;q;λj.rat2real(fst((b j))))
7. ∀i:ℕk. ((fst((c i))) = (snd((c i))) ∈ ℚ)
8. ∀i:ℕk. ((fst((b i))) = (snd((b i))) ∈ ℚ)
9. ∀i:ℕk. ((fst((c i))) = (fst((b i))) ∈ ℚ)
10. x : ℕk
⊢ (c x) = (b x) ∈ ℚInterval

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}b:\mBbbQ{}Cube(k).  \mforall{}q:\mBbbR{}\^{}k.  \mforall{}c:\mBbbQ{}Cube(k).
    ((in-rat-cube(k;q;c)  \mwedge{}  in-rat-cube(k;q;b)  \mwedge{}  (dim(c)  =  0)  \mwedge{}  (dim(b)  =  0))  {}\mRightarrow{}  (c  =  b))


By

---

Latex:
(Auto
  THEN  (All  (RWO  "in-0-dim-cube")  THENA  Auto)
  THEN  (Assert  req-vec(k;\mlambda{}j.rat2real(fst((c  j)));\mlambda{}j.rat2real(fst((b  j))))  BY
                          (RelRST  THEN  Auto))
  THEN  RepUR  ``req-vec``  -1
  THEN  (RWO  "req-rat2real"  (-1)  THENA  Auto)
  THEN  (All  (RWO  "rat-cube-dimension-zero")  THENA  Auto)
  THEN  Unfold  `rational-cube`  0
  THEN  FunExt
  THEN  Auto)

---

Home Index