---

Step * 1 of Lemma iproper-approx


1. I : Interval
2. iproper(I)
3. n : ℕ+
4. icompact(i-approx(I;n))
⊢ icompact(i-approx(I;n + 1))
BY
{ ((D -1 THEN D -2) THEN Using [`r',⌜r⌝] (BLemma `i-approx-compact`)⋅ THEN Auto) }

1
1. I : Interval
2. iproper(I)
3. n : ℕ+
4. r : ℝ
5. r ∈ i-approx(I;n)
6. i-closed(i-approx(I;n))
7. i-finite(i-approx(I;n))
⊢ r ∈ i-approx(I;n + 1)

---

Latex:

---

Latex:

1.  I  :  Interval
2.  iproper(I)
3.  n  :  \mBbbN{}\msupplus{}
4.  icompact(i-approx(I;n))
\mvdash{}  icompact(i-approx(I;n  +  1))


By

---

Latex:
((D  -1  THEN  D  -2)  THEN  Using  [`r',\mkleeneopen{}r\mkleeneclose{}]  (BLemma  `i-approx-compact`)\mcdot{}  THEN  Auto)

---

Home Index