---

Step * 1 of Lemma rat-complex-diameter-bound


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)
BY
{ ((FLemma `rat-cube-diameter-bound` [-1;-2] THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN ThinVar `x'
   THEN ThinVar `y'
   THEN RepeatFor 2 (D -1)
   THEN (RWO "-1" 0 THENA Auto)
   THEN ThinVar `c') }

1
1. k : ℕ
2. K : ℚCube(k) List
3. 0 < ||K||
4. i : ℕ
5. i < ||K||
⊢ rat-cube-diameter(k;K[i]) ≤ rat-complex-diameter(k;K)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  K  :  \mBbbQ{}Cube(k)  List
3.  0  <  ||K||
4.  x  :  \mBbbR{}\^{}k
5.  y  :  \mBbbR{}\^{}k
6.  c  :  \mBbbQ{}Cube(k)
7.  (c  \mmember{}  K)
8.  in-rat-cube(k;y;c)
9.  in-rat-cube(k;x;c)
\mvdash{}  mdist(rn-prod-metric(k);x;y)  \mleq{}  rat-complex-diameter(k;K)


By

---

Latex:
((FLemma  `rat-cube-diameter-bound`  [-1;-2]  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  ThinVar  `x'
  THEN  ThinVar  `y'
  THEN  RepeatFor  2  (D  -1)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  ThinVar  `c')

---

Home Index