---

Step * of Lemma rat-complex-diameter-bound

∀[k:ℕ]. ∀[K:ℚCube(k) List].
  ∀[x,y:ℝ^k].
    mdist(rn-prod-metric(k);x;y) ≤ rat-complex-diameter(k;K) 
    supposing ¬¬(∃c:ℚCube(k). ((c ∈ K) ∧ in-rat-cube(k;y;c) ∧ in-rat-cube(k;x;c))) 
  supposing 0 < ||K||
BY
{ (Auto
   THEN StableCases ⌜∃c:ℚCube(k). ((c ∈ K) ∧ in-rat-cube(k;y;c) ∧ in-rat-cube(k;x;c))⌝⋅
   THEN Auto
   THEN Thin (-2)
   THEN ExRepD) }

1
1. k : ℕ
2. K : ℚCube(k) List
3. 0 < ||K||
4. x : ℝ^k
5. y : ℝ^k
6. c : ℚCube(k)
7. (c ∈ K)
8. in-rat-cube(k;y;c)
9. in-rat-cube(k;x;c)
⊢ mdist(rn-prod-metric(k);x;y) ≤ rat-complex-diameter(k;K)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[K:\mBbbQ{}Cube(k)  List].
    \mforall{}[x,y:\mBbbR{}\^{}k].
        mdist(rn-prod-metric(k);x;y)  \mleq{}  rat-complex-diameter(k;K) 
        supposing  \mneg{}\mneg{}(\mexists{}c:\mBbbQ{}Cube(k).  ((c  \mmember{}  K)  \mwedge{}  in-rat-cube(k;y;c)  \mwedge{}  in-rat-cube(k;x;c))) 
    supposing  0  <  ||K||


By

---

Latex:
(Auto
  THEN  StableCases  \mkleeneopen{}\mexists{}c:\mBbbQ{}Cube(k).  ((c  \mmember{}  K)  \mwedge{}  in-rat-cube(k;y;c)  \mwedge{}  in-rat-cube(k;x;c))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Thin  (-2)
  THEN  ExRepD)

---

Home Index