---

Step * of Lemma icompact-is-subinterval

∀I:Interval. (icompact(I) ⇒ (∃n:ℕ+. I ⊆ i-approx((-∞, ∞);n) ))
BY
{ (Auto
   THEN RepUR ``i-approx`` 0
   THEN ((InstLemma `r-archimedean` [⌜right-endpoint(I)⌝]⋅ THENA Auto)
         THEN (InstLemma `r-archimedean` [⌜left-endpoint(I)⌝]⋅ THENA Auto)
         )
   THEN ExRepD
   THEN D 0 With ⌜imax(n + 1;n1 + 1)⌝ 
   THEN Auto) }

1
1. I : Interval
2. icompact(I)
3. n1 : ℕ
4. r(-n1) ≤ right-endpoint(I)
5. right-endpoint(I) ≤ r(n1)
6. n : ℕ
7. r(-n) ≤ left-endpoint(I)
8. left-endpoint(I) ≤ r(n)
⊢ I ⊆ [r(-imax(n + 1;n1 + 1)), r(imax(n + 1;n1 + 1))] 

---

Latex:

---

Latex:
\mforall{}I:Interval.  (icompact(I)  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}\msupplus{}.  I  \msubseteq{}  i-approx((-\minfty{},  \minfty{});n)  ))


By

---

Latex:
(Auto
  THEN  RepUR  ``i-approx``  0
  THEN  ((InstLemma  `r-archimedean`  [\mkleeneopen{}right-endpoint(I)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `r-archimedean`  [\mkleeneopen{}left-endpoint(I)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              )
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}imax(n  +  1;n1  +  1)\mkleeneclose{} 
  THEN  Auto)

---

Home Index