---

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


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))))
BY
{ (RepeatFor 2 (((D 5 With ⌜i⌝  THENA Auto) THEN MoveToConcl (-1)))
   THEN GenConclTerms Auto [⌜x i⌝;⌜y i⌝;⌜c i⌝]⋅
   THEN All Thin
   THEN D -1
   THEN RepUR ``rmetric`` 0
   THEN (GenConcl ⌜rat2real(v3) = a ∈ ℝ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜rat2real(v4) = b ∈ ℝ⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. v : ℝ
2. v1 : ℝ
3. a : ℝ
4. b : ℝ
5. a ≤ v1
6. v1 ≤ b
7. a ≤ v
8. v ≤ b
⊢ |v - v1| ≤ rmax(r0;b - a)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  x  :  \mBbbR{}\^{}k
4.  y  :  \mBbbR{}\^{}k
5.  in-rat-cube(k;x;c)
6.  in-rat-cube(k;y;c)
7.  i  :  \mBbbZ{}
8.  0  \mleq{}  i
9.  i  \mleq{}  (k  -  1)
\mvdash{}  (rmetric()  (x  i)  (y  i))  \mleq{}  rmax(r0;rat2real(snd((c  i)))  -  rat2real(fst((c  i))))


By

---

Latex:
(RepeatFor  2  (((D  5  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)  THEN  MoveToConcl  (-1)))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}x  i\mkleeneclose{};\mkleeneopen{}y  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  D  -1
  THEN  RepUR  ``rmetric``  0
  THEN  (GenConcl  \mkleeneopen{}rat2real(v3)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}rat2real(v4)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index