---

Step * of Lemma rat-cube-diameter-bound

∀[k:ℕ]. ∀[c:ℚCube(k)]. ∀[x,y:ℝ^k].
  (mdist(rn-prod-metric(k);x;y) ≤ rat-cube-diameter(k;c)) supposing (in-rat-cube(k;y;c) and in-rat-cube(k;x;c))
BY
{ ((Auto THEN RepUR ``mdist rn-prod-metric rat-cube-diameter prod-metric`` 0)
   THEN (BLemma `rsum_functionality_wrt_rleq` THENM D 0)
   THEN Auto) }

1
1. k : ℕ
2. c : ℚCube(k)
3. x : ℝ^k
4. y : ℝ^k
5. in-rat-cube(k;x;c)
6. in-rat-cube(k;y;c)
7. i : ℤ
8. 0 ≤ i
9. i ≤ (k - 1)
⊢ (rmetric() (x i) (y i)) ≤ rmax(r0;rat2real(snd((c i))) - rat2real(fst((c i))))

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c:\mBbbQ{}Cube(k)].  \mforall{}[x,y:\mBbbR{}\^{}k].
    (mdist(rn-prod-metric(k);x;y)  \mleq{}  rat-cube-diameter(k;c))  supposing 
          (in-rat-cube(k;y;c)  and 
          in-rat-cube(k;x;c))


By

---

Latex:
((Auto  THEN  RepUR  ``mdist  rn-prod-metric  rat-cube-diameter  prod-metric``  0)
  THEN  (BLemma  `rsum\_functionality\_wrt\_rleq`  THENM  D  0)
  THEN  Auto)

---

Home Index