---

Step * 1 2 of Lemma rat-sub-div-diameter


1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. 0 < ||K||
5. 0 < ||(K)'||
6. v : ℚCube(k) List
7. no_repeats(ℚCube(k);v)
8. (∀c,d∈v.  Compatible(c;d))
9. (∀c∈v.dim(c) = n ∈ ℤ)
10. (K)' = v ∈ n-dim-complex
11. k@0 : ℕ(||v|| - 1) + 1
⊢ rat-cube-diameter(k;v[k@0]) ≤ ((r1/r(2)) * rmaximum(0;||K|| - 1;i.rat-cube-diameter(k;K[i])))
BY
{ (RenameVar `i' (-1)
   THEN (Assert (v[i] ∈ (K)') BY
               (RWO "-2<" 0 THEN Auto))
   THEN (RWO "member-rat-complex-subdiv2" (-1) THENA Auto)
   THEN ExRepD
   THEN (FLemma `rat-half-cube-diameter` [-1] THENA Auto)
   THEN (RWO  "-1" 0 THENA Auto)) }

1
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. 0 < ||K||
5. 0 < ||(K)'||
6. v : ℚCube(k) List
7. no_repeats(ℚCube(k);v)
8. (∀c,d∈v.  Compatible(c;d))
9. (∀c∈v.dim(c) = n ∈ ℤ)
10. (K)' = v ∈ n-dim-complex
11. i : ℕ(||v|| - 1) + 1
12. a : ℚCube(k)
13. (a ∈ K)
14. ↑is-half-cube(k;v[i];a)
15. rat-cube-diameter(k;v[i]) = ((r1/r(2)) * rat-cube-diameter(k;a))
⊢ ((r1/r(2)) * rat-cube-diameter(k;a)) ≤ ((r1/r(2)) * rmaximum(0;||K|| - 1;i.rat-cube-diameter(k;K[i])))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  K  :  n-dim-complex
4.  0  <  ||K||
5.  0  <  ||(K)'||
6.  v  :  \mBbbQ{}Cube(k)  List
7.  no\_repeats(\mBbbQ{}Cube(k);v)
8.  (\mforall{}c,d\mmember{}v.    Compatible(c;d))
9.  (\mforall{}c\mmember{}v.dim(c)  =  n)
10.  (K)'  =  v
11.  k@0  :  \mBbbN{}(||v||  -  1)  +  1
\mvdash{}  rat-cube-diameter(k;v[k@0])  \mleq{}  ((r1/r(2))  *  rmaximum(0;||K||  -  1;i.rat-cube-diameter(k;K[i])))


By

---

Latex:
(RenameVar  `i'  (-1)
  THEN  (Assert  (v[i]  \mmember{}  (K)')  BY
                          (RWO  "-2<"  0  THEN  Auto))
  THEN  (RWO  "member-rat-complex-subdiv2"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (FLemma  `rat-half-cube-diameter`  [-1]  THENA  Auto)
  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index