---

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


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)))))
BY
{ ((D -4 With ⌜i⌝  THENA Auto) THEN MoveToConcl (-1) THEN GenConclTerms Auto [⌜h i⌝;⌜c i⌝]⋅ THEN All Thin) }

1
1. v : ℚInterval
2. v1 : ℚInterval
⊢ (↑is-half-interval(v;v1))
⇒ (rmax(r0;rat2real(snd(v)) - rat2real(fst(v))) = ((r1/r(2)) * rmax(r0;rat2real(snd(v1)) - rat2real(fst(v1)))))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  h  :  \mBbbQ{}Cube(k)
4.  \mforall{}i:\mBbbN{}k.  (\muparrow{}is-half-interval(h  i;c  i))
5.  i  :  \mBbbZ{}
6.  0  \mleq{}  i
7.  i  \mleq{}  (k  -  1)
\mvdash{}  rmax(r0;rat2real(snd((h  i)))  -  rat2real(fst((h  i))))
=  ((r1/r(2))  *  rmax(r0;rat2real(snd((c  i)))  -  rat2real(fst((c  i)))))


By

---

Latex:
((D  -4  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}h  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin)

---

Home Index