---

Step * 1 2 1 1 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. 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]))
BY
{ (RWO  "-1" 0 THEN 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. i1 : ℕ
14. i1 < ||K||
15. a = K[i1] ∈ ℚCube(k)
⊢ rat-cube-diameter(k;K[i1]) ≤ 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.  i1  :  \mBbbN{}
14.  i1  <  ||K||
15.  a  =  K[i1]
\mvdash{}  rat-cube-diameter(k;a)  \mleq{}  rmaximum(0;||K||  -  1;i.rat-cube-diameter(k;K[i]))


By

---

Latex:
(RWO    "-1"  0  THEN  Auto)

---

Home Index