---

Step * of Lemma rat-complex-iter-subdiv-diameter

∀[k,n:ℕ]. ∀[K:{K:n-dim-complex| 0 < ||K||} ]. ∀[j:ℕ].
  (rat-complex-diameter(k;K'^(j)) ≤ ((r1/r(2^j)) * rat-complex-diameter(k;K)))
BY
{ (Auto THEN NatInd (-1)) }

1
.....basecase..... 
1. k : ℕ
2. n : ℕ
3. K : {K:n-dim-complex| 0 < ||K||} 
4. j : ℤ
⊢ rat-complex-diameter(k;K'^(0)) ≤ ((r1/r(2^0)) * rat-complex-diameter(k;K))

2
.....upcase..... 
1. k : ℕ
2. n : ℕ
3. K : {K:n-dim-complex| 0 < ||K||} 
4. j : ℤ
5. 0 < j
6. rat-complex-diameter(k;K'^(j - 1)) ≤ ((r1/r(2^(j - 1))) * rat-complex-diameter(k;K))
⊢ rat-complex-diameter(k;K'^(j)) ≤ ((r1/r(2^j)) * rat-complex-diameter(k;K))

---

Latex:

---

Latex:
\mforall{}[k,n:\mBbbN{}].  \mforall{}[K:\{K:n-dim-complex|  0  <  ||K||\}  ].  \mforall{}[j:\mBbbN{}].
    (rat-complex-diameter(k;K'\^{}(j))  \mleq{}  ((r1/r(2\^{}j))  *  rat-complex-diameter(k;K)))


By

---

Latex:
(Auto  THEN  NatInd  (-1))

---

Home Index