---

Step * of Lemma compact-subinterval

∀I:Interval. ∀J:{J:Interval| icompact(J)} .  (J ⊆ I  ⇒ (∃n:{n:ℕ+| icompact(i-approx(I;n))} . J ⊆ i-approx(I;n) ))
BY
{ (Auto
   THEN (Assert icompact(J) BY
               (DVar `J'⋅ THEN Unhide THEN Auto))
   THEN (InstLemma `i-member-compact` [⌜J⌝]⋅ THENA Auto)
   THEN (InstLemma `icompact-endpoints` [⌜J⌝]⋅ THENA Auto)
   THEN (InstLemma `i-member-iff` [⌜I⌝]⋅ THENA Auto)) }

1
1. I : Interval
2. J : {J:Interval| icompact(J)} 
3. J ⊆ I 
4. icompact(J)
5. ∀r:ℝ. (r ∈ J ⇐⇒ left-endpoint(J)≤r≤right-endpoint(J))
6. (left-endpoint(J) ∈ J) ∧ (right-endpoint(J) ∈ J)
7. ∀r:ℝ. (r ∈ I ⇐⇒ ∃n:ℕ+. (r ∈ i-approx(I;n)))
⊢ ∃n:{n:ℕ+| icompact(i-approx(I;n))} . J ⊆ i-approx(I;n) 

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  icompact(J)  BY
                          (DVar  `J'\mcdot{}  THEN  Unhide  THEN  Auto))
  THEN  (InstLemma  `i-member-compact`  [\mkleeneopen{}J\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `icompact-endpoints`  [\mkleeneopen{}J\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `i-member-iff`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index