---

Step * 1 1 of Lemma continuous-range-totally-bounded

.....wf..... 
1. m : ℕ+
2. e : ℝ
3. r0 < e
4. k : ℕ+
5. (r1/r(k)) < e
6. d : ℝ
7. I : Interval
8. icompact(I)
9. f : I ⟶ℝ
10. r0 < d
11. ∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
12. p : partition(I)
13. partition-mesh(I;p) ≤ d
⊢ ||full-partition(I;p)|| ∈ ℕ+
BY
{ (RepUR ``full-partition`` 0 THEN Auto')⋅ }

---

Latex:

---

Latex:
.....wf..... 
1.  m  :  \mBbbN{}\msupplus{}
2.  e  :  \mBbbR{}
3.  r0  <  e
4.  k  :  \mBbbN{}\msupplus{}
5.  (r1/r(k))  <  e
6.  d  :  \mBbbR{}
7.  I  :  Interval
8.  icompact(I)
9.  f  :  I  {}\mrightarrow{}\mBbbR{}
10.  r0  <  d
11.  \mforall{}x,y:\mBbbR{}.    ((x  \mmember{}  I)  {}\mRightarrow{}  (y  \mmember{}  I)  {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(k))))
12.  p  :  partition(I)
13.  partition-mesh(I;p)  \mleq{}  d
\mvdash{}  ||full-partition(I;p)||  \mmember{}  \mBbbN{}\msupplus{}


By

---

Latex:
(RepUR  ``full-partition``  0  THEN  Auto')\mcdot{}

---

Home Index