---

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

.....assertion..... 
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))
⊢ rat-cube-diameter(k;a) ≤ rmaximum(0;||K|| - 1;i.rat-cube-diameter(k;K[i]))
BY
{ (RepeatFor 2 (Thin (-1)) THEN RepeatFor 2 (D -1)) }

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. i1 : ℕ
14. i1 < ||K||
15. a = K[i1] ∈ ℚCube(k)
⊢ rat-cube-diameter(k;a) ≤ rmaximum(0;||K|| - 1;i.rat-cube-diameter(k;K[i]))

---

Latex:

---

Latex:
.....assertion..... 
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.  i  :  \mBbbN{}(||v||  -  1)  +  1
12.  a  :  \mBbbQ{}Cube(k)
13.  (a  \mmember{}  K)
14.  \muparrow{}is-half-cube(k;v[i];a)
15.  rat-cube-diameter(k;v[i])  =  ((r1/r(2))  *  rat-cube-diameter(k;a))
\mvdash{}  rat-cube-diameter(k;a)  \mleq{}  rmaximum(0;||K||  -  1;i.rat-cube-diameter(k;K[i]))


By

---

Latex:
(RepeatFor  2  (Thin  (-1))  THEN  RepeatFor  2  (D  -1))

---

Home Index