---

Step * 1 2 1 2 2 1 1 2 1 of Lemma nearby-increasing-partition

.....assertion..... 
1. I : Interval
2. icompact(I)
3. p : ℝ List
4. ¬(p = [] ∈ (ℝ List))
5. e : {e:ℝ| r0 < e} 
6. k : ℕ+
7. (r1/r(k)) < e
8. left-endpoint(I) < right-endpoint(I)
9. partitions(I;p)
10. last(p) < right-endpoint(I)
11. k1 : ℕ+
12. (r1/r(k1)) < (right-endpoint(I) - last(p))
13. N : ℕ+
14. ∀i:ℕ||p||. (((r(i)/r(N)) < e) ∧ ((r(i)/r(N)) < (right-endpoint(I) - last(p))))
⊢ frs-increasing(mklist(||p||;λj.(p[j] + (r(j)/r(N)))))
BY
{ ((D 0 THEN RWO "mklist_length" 0 THEN Auto)
   THEN (RWO "select-mklist" 0 THENA Auto)
   THEN Reduce 0
   THEN (Assert p[i] ≤ p[j] BY
               Auto)
   THEN (RWO "-1" 0 THENA Auto)) }

1
1. I : Interval
2. icompact(I)
3. p : ℝ List
4. ¬(p = [] ∈ (ℝ List))
5. e : {e:ℝ| r0 < e} 
6. k : ℕ+
7. (r1/r(k)) < e
8. left-endpoint(I) < right-endpoint(I)
9. partitions(I;p)
10. last(p) < right-endpoint(I)
11. k1 : ℕ+
12. (r1/r(k1)) < (right-endpoint(I) - last(p))
13. N : ℕ+
14. ∀i:ℕ||p||. (((r(i)/r(N)) < e) ∧ ((r(i)/r(N)) < (right-endpoint(I) - last(p))))
15. i : ℕ||mklist(||p||;λj.(p[j] + (r(j)/r(N))))||
16. j : ℕ||p||
17. i < j
18. p[i] ≤ p[j]
⊢ (p[j] + (r(i)/r(N))) < (p[j] + (r(j)/r(N)))

---

Latex:

---

Latex:
.....assertion..... 
1.  I  :  Interval
2.  icompact(I)
3.  p  :  \mBbbR{}  List
4.  \mneg{}(p  =  [])
5.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
6.  k  :  \mBbbN{}\msupplus{}
7.  (r1/r(k))  <  e
8.  left-endpoint(I)  <  right-endpoint(I)
9.  partitions(I;p)
10.  last(p)  <  right-endpoint(I)
11.  k1  :  \mBbbN{}\msupplus{}
12.  (r1/r(k1))  <  (right-endpoint(I)  -  last(p))
13.  N  :  \mBbbN{}\msupplus{}
14.  \mforall{}i:\mBbbN{}||p||.  (((r(i)/r(N))  <  e)  \mwedge{}  ((r(i)/r(N))  <  (right-endpoint(I)  -  last(p))))
\mvdash{}  frs-increasing(mklist(||p||;\mlambda{}j.(p[j]  +  (r(j)/r(N)))))


By

---

Latex:
((D  0  THEN  RWO  "mklist\_length"  0  THEN  Auto)
  THEN  (RWO  "select-mklist"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Assert  p[i]  \mleq{}  p[j]  BY
                          Auto)
  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index