---

Step * 2 1 of Lemma iproper-approx


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))
BY
{ ((Assert (r1/r(n + 1)) < (r1/r(n)) BY Auto) THEN (Assert r(n) < r(n + 1) BY Auto)) }

1
1. I : Interval
2. iproper(I)
3. n : ℕ+
4. left-endpoint(i-approx(I;n)) ≤ right-endpoint(i-approx(I;n))
5. (r1/r(n + 1)) < (r1/r(n))
6. r(n) < r(n + 1)
⊢ iproper(i-approx(I;n + 1))

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  (r1/r(n  +  1))  <  (r1/r(n))  BY  Auto)  THEN  (Assert  r(n)  <  r(n  +  1)  BY  Auto))

---

Home Index