---

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

∀I:Interval. ∀f:I ⟶ℝ.  (icompact(I) ⇒ f[x] continuous for x ∈ I ⇒ totally-bounded(f[x](x∈I)))
BY
{ (Auto
   THEN InstLemma `continuous-range-totally-bounded` [⌜I⌝;⌜f⌝;⌜1⌝]⋅
   THEN Auto
   THEN All (Unfold `so_apply`)⋅
   THEN (All (RWO "i-approx-of-compact") THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.    (icompact(I)  {}\mRightarrow{}  f[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  totally-bounded(f[x](x\mmember{}I)))


By

---

Latex:
(Auto
  THEN  InstLemma  `continuous-range-totally-bounded`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All  (Unfold  `so\_apply`)\mcdot{}
  THEN  (All  (RWO  "i-approx-of-compact")  THEN  Auto)\mcdot{})

---

Home Index