---

Step * of Lemma rat-half-cube-diameter

∀[k:ℕ]. ∀[c,h:ℚCube(k)].  rat-cube-diameter(k;h) = ((r1/r(2)) * rat-cube-diameter(k;c)) supposing ↑is-half-cube(k;h;c)
BY
{ (Auto
   THEN (RWO "assert-is-half-cube" (-1) THENA Auto)
   THEN Unfold `rat-cube-diameter` 0
   THEN (RWO "rsum_linearity2<" 0 THENA Auto)
   THEN (BLemma `rsum_functionality` THENM D 0)
   THEN Auto) }

1
1. k : ℕ
2. c : ℚCube(k)
3. h : ℚCube(k)
4. ∀i:ℕk. (↑is-half-interval(h i;c i))
5. i : ℤ
6. 0 ≤ i
7. i ≤ (k - 1)
⊢ rmax(r0;rat2real(snd((h i))) - rat2real(fst((h i))))
= ((r1/r(2)) * rmax(r0;rat2real(snd((c i))) - rat2real(fst((c i)))))

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c,h:\mBbbQ{}Cube(k)].
    rat-cube-diameter(k;h)  =  ((r1/r(2))  *  rat-cube-diameter(k;c))  supposing  \muparrow{}is-half-cube(k;h;c)


By

---

Latex:
(Auto
  THEN  (RWO  "assert-is-half-cube"  (-1)  THENA  Auto)
  THEN  Unfold  `rat-cube-diameter`  0
  THEN  (RWO  "rsum\_linearity2<"  0  THENA  Auto)
  THEN  (BLemma  `rsum\_functionality`  THENM  D  0)
  THEN  Auto)

---

Home Index