---

Step * of Lemma continuous-range-totally-bounded

∀I:Interval. ∀f:I ⟶ℝ.
  (f[x] continuous for x ∈ I ⇒ (∀m:ℕ+. (i-nonvoid(i-approx(I;m)) ⇒ totally-bounded(f[x](x∈i-approx(I;m))))))
BY
{ (Auto
   THEN (With ⌜m⌝ (D (-3))⋅ THENA (Auto THEN MemTypeCD THEN Auto))
   THEN UnfoldTopAb 0
   THEN Auto
   THEN (InstLemma `small-reciprocal-real` [⌜e⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (InstHyp [⌜k⌝] 5⋅ THENA Auto)
   THEN Thin 5
   THEN D -1
   THEN (Assert icompact(i-approx(I;m)) BY
               (D 0 THEN Auto))
   THEN (Assert i-approx(I;m) ⊆ I  BY
               Auto)
   THEN (Assert (r0 < d)
               ∧ (∀x,y:ℝ.
                    ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))) BY
               (Unhide THEN Auto))
   THEN Thin (-4)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN (GenConcl ⌜i-approx(I;m) = J ∈ Interval⌝⋅ THENA Auto)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN GenConcl ⌜f = g ∈ J ⟶ℝ⌝⋅
   THEN Auto
   THEN ThinVar `f'
   THEN ThinVar `I'
   THEN RenameTo `I' `J'
   THEN RenameTo `f' `g') }

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))))
⊢ ∃n:ℕ+. ∃a:ℕn ⟶ ℝ. ((∀i:ℕn. (a i ∈ f[x](x∈I))) ∧ (∀x:ℝ. ((x ∈ f[x](x∈I)) ⇒ (∃i:ℕn. (|x - a i| < e)))))

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    (f[x]  continuous  for  x  \mmember{}  I
    {}\mRightarrow{}  (\mforall{}m:\mBbbN{}\msupplus{}.  (i-nonvoid(i-approx(I;m))  {}\mRightarrow{}  totally-bounded(f[x](x\mmember{}i-approx(I;m))))))


By

---

Latex:
(Auto
  THEN  (With  \mkleeneopen{}m\mkleeneclose{}  (D  (-3))\mcdot{}  THENA  (Auto  THEN  MemTypeCD  THEN  Auto))
  THEN  UnfoldTopAb  0
  THEN  Auto
  THEN  (InstLemma  `small-reciprocal-real`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}k\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  Thin  5
  THEN  D  -1
  THEN  (Assert  icompact(i-approx(I;m))  BY
                          (D  0  THEN  Auto))
  THEN  (Assert  i-approx(I;m)  \msubseteq{}  I    BY
                          Auto)
  THEN  (Assert  (r0  <  d)
                          \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                    ((x  \mmember{}  i-approx(I;m))
                                    {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
                                    {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
                                    {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(k)))))  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  (-4)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}i-approx(I;m)  =  J\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  GenConcl  \mkleeneopen{}f  =  g\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  ThinVar  `f'
  THEN  ThinVar  `I'
  THEN  RenameTo  `I'  `J'
  THEN  RenameTo  `f'  `g')

---

Home Index