---

Step * of Lemma fine-iter-subdiv

∀k:ℕ
  ∀[n:ℕ]
    ∀K:{K:n-dim-complex| 0 < ||K||} . ∀M:ℕ+.
      ∃j:ℕ
       ∀[x,y:ℝ^k].
         mdist(rn-prod-metric(k);x;y) ≤ (r1/r(M)) 
         supposing ¬¬(∃c:ℚCube(k). ((c ∈ K'^(j)) ∧ in-rat-cube(k;y;c) ∧ in-rat-cube(k;x;c)))
BY
{ (InstLemma `rat-complex-iter-subdiv-diameter` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (Assert ∀[j:ℕ]. ∀[x,y:ℝ^k].
                  mdist(rn-prod-metric(k);x;y) ≤ ((r1/r(2^j)) * rat-complex-diameter(k;K)) 
                  supposing ¬¬(∃c:ℚCube(k). ((c ∈ K'^(j)) ∧ in-rat-cube(k;y;c) ∧ in-rat-cube(k;x;c))) BY
               ((D 0 THENA Auto)
                THEN (InstLemma `rat-complex-diameter-bound` [⌜k⌝;⌜K'^(j)⌝]⋅ THENM RWO "4<" 0)
                THEN Auto))
   THEN (Assert ⌜∃j:ℕ. (((r1/r(2^j)) * rat-complex-diameter(k;K)) ≤ (r1/r(M)))⌝⋅
   THENM (ParallelLast THEN RWO "-1<" 0 THEN Auto)
   )) }

1
.....assertion..... 
1. k : ℕ
2. [n] : ℕ
3. K : {K:n-dim-complex| 0 < ||K||} 
4. ∀[j:ℕ]. (rat-complex-diameter(k;K'^(j)) ≤ ((r1/r(2^j)) * rat-complex-diameter(k;K)))
5. M : ℕ+
6. ∀[j:ℕ]. ∀[x,y:ℝ^k].
     mdist(rn-prod-metric(k);x;y) ≤ ((r1/r(2^j)) * rat-complex-diameter(k;K)) 
     supposing ¬¬(∃c:ℚCube(k). ((c ∈ K'^(j)) ∧ in-rat-cube(k;y;c) ∧ in-rat-cube(k;x;c)))
⊢ ∃j:ℕ. (((r1/r(2^j)) * rat-complex-diameter(k;K)) ≤ (r1/r(M)))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}
    \mforall{}[n:\mBbbN{}]
        \mforall{}K:\{K:n-dim-complex|  0  <  ||K||\}  .  \mforall{}M:\mBbbN{}\msupplus{}.
            \mexists{}j:\mBbbN{}
              \mforall{}[x,y:\mBbbR{}\^{}k].
                  mdist(rn-prod-metric(k);x;y)  \mleq{}  (r1/r(M)) 
                  supposing  \mneg{}\mneg{}(\mexists{}c:\mBbbQ{}Cube(k).  ((c  \mmember{}  K'\^{}(j))  \mwedge{}  in-rat-cube(k;y;c)  \mwedge{}  in-rat-cube(k;x;c)))


By

---

Latex:
(InstLemma  `rat-complex-iter-subdiv-diameter`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  \mforall{}[j:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}k].
                                mdist(rn-prod-metric(k);x;y)  \mleq{}  ((r1/r(2\^{}j))  *  rat-complex-diameter(k;K)) 
                                supposing  \mneg{}\mneg{}(\mexists{}c:\mBbbQ{}Cube(k)
                                                            ((c  \mmember{}  K'\^{}(j))  \mwedge{}  in-rat-cube(k;y;c)  \mwedge{}  in-rat-cube(k;x;c)))  BY
                          ((D  0  THENA  Auto)
                            THEN  (InstLemma  `rat-complex-diameter-bound`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}K'\^{}(j)\mkleeneclose{}]\mcdot{}  THENM  RWO  "4<"  0)
                            THEN  Auto))
  THEN  (Assert  \mkleeneopen{}\mexists{}j:\mBbbN{}.  (((r1/r(2\^{}j))  *  rat-complex-diameter(k;K))  \mleq{}  (r1/r(M)))\mkleeneclose{}\mcdot{}
  THENM  (ParallelLast  THEN  RWO  "-1<"  0  THEN  Auto)
  ))

---

Home Index