---

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


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
14. ∀i:ℕ||full-partition(I;p)||. ((λi.f(full-partition(I;p)[i])) i ∈ f[x](x∈I))
15. y : ℝ
16. x : ℝ
17. x ∈ I
18. f[x] = y
19. i : ℕ||full-partition(I;p)||
20. |x - full-partition(I;p)[i]| ≤ d
21. ∀I:Interval. (icompact(I) ⇒ (∀p:partition(I). (∀x∈full-partition(I;p).x ∈ I)))
22. full-partition(I;p)[i] ∈ I
⊢ |y - f(full-partition(I;p)[i])| < e
BY
{ (AllHyps (\h. Unfold `so_apply` h THEN Fold `r-ap` h)⋅
   THEN (Assert |f(x) - f(full-partition(I;p)[i])| ≤ (r1/r(k)) BY
               (BackThruSomeHyp THEN Auto))
   ) }

1
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
14. ∀i:ℕ||full-partition(I;p)||. (λi.f(full-partition(I;p)[i])(i) ∈ f(x)(x∈I))
15. y : ℝ
16. x : ℝ
17. x ∈ I
18. f(x) = y
19. i : ℕ||full-partition(I;p)||
20. |x - full-partition(I;p)[i]| ≤ d
21. ∀I:Interval. (icompact(I) ⇒ (∀p:partition(I). (∀x∈full-partition(I;p).x ∈ I)))
22. full-partition(I;p)[i] ∈ I
23. |f(x) - f(full-partition(I;p)[i])| ≤ (r1/r(k))
⊢ |y - f(full-partition(I;p)[i])| < e

---

Latex:

---

Latex:

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
14.  \mforall{}i:\mBbbN{}||full-partition(I;p)||.  ((\mlambda{}i.f(full-partition(I;p)[i]))  i  \mmember{}  f[x](x\mmember{}I))
15.  y  :  \mBbbR{}
16.  x  :  \mBbbR{}
17.  x  \mmember{}  I
18.  f[x]  =  y
19.  i  :  \mBbbN{}||full-partition(I;p)||
20.  |x  -  full-partition(I;p)[i]|  \mleq{}  d
21.  \mforall{}I:Interval.  (icompact(I)  {}\mRightarrow{}  (\mforall{}p:partition(I).  (\mforall{}x\mmember{}full-partition(I;p).x  \mmember{}  I)))
22.  full-partition(I;p)[i]  \mmember{}  I
\mvdash{}  |y  -  f(full-partition(I;p)[i])|  <  e


By

---

Latex:
(AllHyps  (\mbackslash{}h.  Unfold  `so\_apply`  h  THEN  Fold  `r-ap`  h)\mcdot{}
  THEN  (Assert  |f(x)  -  f(full-partition(I;p)[i])|  \mleq{}  (r1/r(k))  BY
                          (BackThruSomeHyp  THEN  Auto))
  )

---

Home Index