---

Step * 1 2 1 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. 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])))
BY
{ (Assert ⌜rat-cube-diameter(k;a) ≤ rmaximum(0;||K|| - 1;i.rat-cube-diameter(k;K[i]))⌝⋅
THENM ((RWO "rmul_comm" 0 THENA Auto) THEN BLemma `rmul_functionality_wrt_rleq` THEN Auto)
) }

1
.....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]))

---

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.  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{}  ((r1/r(2))  *  rat-cube-diameter(k;a))  \mleq{}  ((r1/r(2))
*  rmaximum(0;||K||  -  1;i.rat-cube-diameter(k;K[i])))


By

---

Latex:
(Assert  \mkleeneopen{}rat-cube-diameter(k;a)  \mleq{}  rmaximum(0;||K||  -  1;i.rat-cube-diameter(k;K[i]))\mkleeneclose{}\mcdot{}
THENM  ((RWO  "rmul\_comm"  0  THENA  Auto)  THEN  BLemma  `rmul\_functionality\_wrt\_rleq`  THEN  Auto)
)

---

Home Index