---

Step * 1 of Lemma i-approx-rep


1. I : Interval
2. n : ℕ+
3. r : ℝ
4. r ∈ i-approx(I;n)
5. icompact(i-approx(I;n))
⊢ ∃a,b:ℝ. ((a ≤ b) ∧ (i-approx(I;n) = [a, b] ∈ Interval))
BY
{ (MoveToConcl (-1) THEN (GenConcl ⌜i-approx(I;n) = J ∈ Interval⌝⋅ THENA Auto) THEN All Thin) }

1
1. J : Interval
⊢ icompact(J) ⇒ (∃a,b:ℝ. ((a ≤ b) ∧ (J = [a, b] ∈ Interval)))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  n  :  \mBbbN{}\msupplus{}
3.  r  :  \mBbbR{}
4.  r  \mmember{}  i-approx(I;n)
5.  icompact(i-approx(I;n))
\mvdash{}  \mexists{}a,b:\mBbbR{}.  ((a  \mleq{}  b)  \mwedge{}  (i-approx(I;n)  =  [a,  b]))


By

---

Latex:
(MoveToConcl  (-1)  THEN  (GenConcl  \mkleeneopen{}i-approx(I;n)  =  J\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)

---

Home Index