---

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


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])))
BY
{ (InstLemma `rmaximum-lub` [⌜0⌝;⌜||(K)'|| - 1⌝;⌜λ2i.rat-cube-diameter(k;(K)'[i])⌝;⌜(r1/r(2))
                                                                                    * rmaximum(0;||K|| 
                                                                                      - 1;i.rat-cube-diameter(k;K[i]))⌝]
   ⋅
   THENA (((GenConclTerm ⌜(K)'⌝⋅ THENA Auto) THEN DVar `v' THEN Auto) ORELSE Auto)
   ) }

1
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. 0 < ||K||
5. 0 < ||(K)'||
6. v : ℚCube(k) List
7. [%6] : no_repeats(ℚCube(k);v) ∧ (∀c,d∈v.  Compatible(c;d)) ∧ (∀c∈v.dim(c) = n ∈ ℤ)
8. (K)' = v ∈ n-dim-complex
⊢ 0 ≤ (||v|| - 1)

2
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])))

3
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. 0 < ||K||
5. 0 < ||(K)'||
6. 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])))
⊢ 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:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  K  :  n-dim-complex
4.  0  <  ||K||
5.  0  <  ||(K)'||
\mvdash{}  rmaximum(0;||(K)'||  -  1;i.rat-cube-diameter(k;(K)'[i]))  \mleq{}  ((r1/r(2))
*  rmaximum(0;||K||  -  1;i.rat-cube-diameter(k;K[i])))


By

---

Latex:
(InstLemma  `rmaximum-lub`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}||(K)'||  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.rat-cube-diameter(k;(K)'[i])\mkleeneclose{};
  \mkleeneopen{}(r1/r(2))  *  rmaximum(0;||K||  -  1;i.rat-cube-diameter(k;K[i]))\mkleeneclose{}]\mcdot{}
  THENA  (((GenConclTerm  \mkleeneopen{}(K)'\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  DVar  `v'  THEN  Auto)  ORELSE  Auto)
  )

---

Home Index