---

Step * 2 of Lemma iproper-approx


1. I : Interval
2. iproper(I)
3. n : ℕ+
4. icompact(i-approx(I;n))
5. icompact(i-approx(I;n + 1))
⊢ iproper(i-approx(I;n + 1))
BY
{ (Thin (-1) THEN (FLemma `icompact-endpoints-rleq` [-1] THENA Auto) THEN Thin (-2)) }

1
1. I : Interval
2. iproper(I)
3. n : ℕ+
4. left-endpoint(i-approx(I;n)) ≤ right-endpoint(i-approx(I;n))
⊢ iproper(i-approx(I;n + 1))

---

Latex:

---

Latex:

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


By

---

Latex:
(Thin  (-1)  THEN  (FLemma  `icompact-endpoints-rleq`  [-1]  THENA  Auto)  THEN  Thin  (-2))

---

Home Index