---

Step * of Lemma iproper-approx

∀I:Interval
  (iproper(I) ⇒ (∀n:ℕ+. (icompact(i-approx(I;n)) ⇒ (icompact(i-approx(I;n + 1)) ∧ iproper(i-approx(I;n + 1))))))
BY
{ Auto }

1
1. I : Interval
2. iproper(I)
3. n : ℕ+
4. icompact(i-approx(I;n))
⊢ icompact(i-approx(I;n + 1))

2
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))

---

Latex:

---

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}
                (icompact(i-approx(I;n))  {}\mRightarrow{}  (icompact(i-approx(I;n  +  1))  \mwedge{}  iproper(i-approx(I;n  +  1))))))


By

---

Latex:
Auto

---

Home Index