---

Step * 1 1 of Lemma compact-subinterval


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
7. right-endpoint(J) ∈ J
8. ∀r:ℝ. (r ∈ I ⇐⇒ ∃n:ℕ+. (r ∈ i-approx(I;n)))
9. n1 : ℕ+
10. left-endpoint(J) ∈ i-approx(I;n1)
11. n : ℕ+
12. right-endpoint(J) ∈ i-approx(I;n)
⊢ ∃n:{n:ℕ+| icompact(i-approx(I;n))} . J ⊆ i-approx(I;n) 
BY
{ (With ⌜imax(n;n1)⌝ (D 0)⋅ THENA Auto) }

1
.....wf..... 
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
7. right-endpoint(J) ∈ J
8. ∀r:ℝ. (r ∈ I ⇐⇒ ∃n:ℕ+. (r ∈ i-approx(I;n)))
9. n1 : ℕ+
10. left-endpoint(J) ∈ i-approx(I;n1)
11. n : ℕ+
12. right-endpoint(J) ∈ i-approx(I;n)
⊢ imax(n;n1) ∈ {n:ℕ+| icompact(i-approx(I;n))} 

2
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
7. right-endpoint(J) ∈ J
8. ∀r:ℝ. (r ∈ I ⇐⇒ ∃n:ℕ+. (r ∈ i-approx(I;n)))
9. n1 : ℕ+
10. left-endpoint(J) ∈ i-approx(I;n1)
11. n : ℕ+
12. right-endpoint(J) ∈ i-approx(I;n)
⊢ J ⊆ i-approx(I;imax(n;n1)) 

---

Latex:

---

Latex:

1.  I  :  Interval
2.  J  :  \{J:Interval|  icompact(J)\} 
3.  J  \msubseteq{}  I 
4.  icompact(J)
5.  \mforall{}r:\mBbbR{}.  (r  \mmember{}  J  \mLeftarrow{}{}\mRightarrow{}  left-endpoint(J)\mleq{}r\mleq{}right-endpoint(J))
6.  left-endpoint(J)  \mmember{}  J
7.  right-endpoint(J)  \mmember{}  J
8.  \mforall{}r:\mBbbR{}.  (r  \mmember{}  I  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}\msupplus{}.  (r  \mmember{}  i-approx(I;n)))
9.  n1  :  \mBbbN{}\msupplus{}
10.  left-endpoint(J)  \mmember{}  i-approx(I;n1)
11.  n  :  \mBbbN{}\msupplus{}
12.  right-endpoint(J)  \mmember{}  i-approx(I;n)
\mvdash{}  \mexists{}n:\{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))\}  .  J  \msubseteq{}  i-approx(I;n) 


By

---

Latex:
(With  \mkleeneopen{}imax(n;n1)\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)

---

Home Index