---

Step * of Lemma proper-continuous-maps-compact

No Annotations
∀I:Interval. ∀f:I ⟶ℝ.  (f[x] (proper)continuous for x ∈ I ⇒ maps-compact-proper(I;(-∞, ∞);x.f[x]))
BY
{ (Auto
   THEN D 0
   THEN (Auto
         THEN (Assert i-approx(I;n) ⊆ I  BY
                     Auto)
         THEN InstLemma `proper-continuous-implies` [⌜I⌝;⌜f⌝;⌜n⌝]⋅
         THEN Auto)
   THEN RenameVar `mc' (-1)
   THEN (InstLemma `range-inf-property` [i-approx(I;n);⌜f⌝;⌜mc⌝]⋅ THENA Auto)
   THEN (InstLemma `range-sup-property` [i-approx(I;n);⌜f⌝;⌜mc⌝]⋅ THENA Auto)) }

1
1. I : Interval
2. f : I ⟶ℝ
3. f[x] (proper)continuous for x ∈ I
4. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
5. i-approx(I;n) ⊆ I 
6. mc : f[x] continuous for x ∈ i-approx(I;n)
7. inf(f[x](x∈i-approx(I;n))) = inf{f[x]|x ∈ i-approx(I;n)}
8. sup(f[x](x∈i-approx(I;n))) = sup{f[x]|x ∈ i-approx(I;n)}
⊢ ∃m:{m:ℕ+| icompact(i-approx((-∞, ∞);m)) ∧ iproper(i-approx((-∞, ∞);m))} 
   ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx((-∞, ∞);m))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.    (f[x]  (proper)continuous  for  x  \mmember{}  I  {}\mRightarrow{}  maps-compact-proper(I;(-\minfty{},  \minfty{});x.f[x]))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  (Auto
              THEN  (Assert  i-approx(I;n)  \msubseteq{}  I    BY
                                      Auto)
              THEN  InstLemma  `proper-continuous-implies`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
              THEN  Auto)
  THEN  RenameVar  `mc'  (-1)
  THEN  (InstLemma  `range-inf-property`  [i-approx(I;n);\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `range-sup-property`  [i-approx(I;n);\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index