---

Step * of Lemma rat-sub-div-diameter

∀[k,n:ℕ]. ∀[K:n-dim-complex].
  rat-complex-diameter(k;(K)') ≤ ((r1/r(2)) * rat-complex-diameter(k;K)) supposing 0 < ||K||
BY
{ (RepeatFor 4 (Intro)
   THEN (Assert 0 < ||(K)'|| BY
               EAuto 1)
   THEN (Unhide THENA Auto)
   THEN Unfold `rat-complex-diameter` 0) }

1
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. 0 < ||K||
5. 0 < ||(K)'||
⊢ rmaximum(0;||(K)'|| - 1;i.rat-cube-diameter(k;(K)'[i])) ≤ ((r1/r(2))
* rmaximum(0;||K|| - 1;i.rat-cube-diameter(k;K[i])))

---

Latex:

---

Latex:
\mforall{}[k,n:\mBbbN{}].  \mforall{}[K:n-dim-complex].
    rat-complex-diameter(k;(K)')  \mleq{}  ((r1/r(2))  *  rat-complex-diameter(k;K))  supposing  0  <  ||K||


By

---

Latex:
(RepeatFor  4  (Intro)
  THEN  (Assert  0  <  ||(K)'||  BY
                          EAuto  1)
  THEN  (Unhide  THENA  Auto)
  THEN  Unfold  `rat-complex-diameter`  0)

---

Home Index