---

Step * 1 of Lemma fine-iter-subdiv

.....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)))
BY
{ ((GenConclTerm ⌜rat-complex-diameter(k;K)⌝⋅ THENA Auto)
   THEN All Thin
   THEN (InstLemma `r-archimedean` [⌜v⌝]⋅ THENA Auto)
   THEN ExRepD) }

1
1. M : ℕ+
2. v : ℝ
3. n : ℕ
4. r(-n) ≤ v
5. v ≤ r(n)
⊢ ∃j:ℕ. (((r1/r(2^j)) * v) ≤ (r1/r(M)))

---

Latex:

---

Latex:
.....assertion..... 
1.  k  :  \mBbbN{}
2.  [n]  :  \mBbbN{}
3.  K  :  \{K:n-dim-complex|  0  <  ||K||\} 
4.  \mforall{}[j:\mBbbN{}].  (rat-complex-diameter(k;K'\^{}(j))  \mleq{}  ((r1/r(2\^{}j))  *  rat-complex-diameter(k;K)))
5.  M  :  \mBbbN{}\msupplus{}
6.  \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)))
\mvdash{}  \mexists{}j:\mBbbN{}.  (((r1/r(2\^{}j))  *  rat-complex-diameter(k;K))  \mleq{}  (r1/r(M)))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}rat-complex-diameter(k;K)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  (InstLemma  `r-archimedean`  [\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index