---

Step * 1 2 1 2 2 2 1 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. i : ℕ||p|| - 1
11. p[i] < p[i + 1]
12. k1 : ℕ+
13. (r1/r(k1)) < (p[i + 1] - p[i])
⊢ ∃N:ℕ+. ∀j:ℕ||p||. (((r(j)/r(N)) < e) ∧ ((r(j)/r(N)) < (p[i + 1] - p[i])))
BY
{ (D 0 With ⌜||p|| * imax(k;k1)⌝  THEN 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. i : ℕ||p|| - 1
11. p[i] < p[i + 1]
12. k1 : ℕ+
13. (r1/r(k1)) < (p[i + 1] - p[i])
14. j : ℕ||p||
⊢ (r(j)/r(||p|| * imax(k;k1))) < e

2
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. i : ℕ||p|| - 1
11. p[i] < p[i + 1]
12. k1 : ℕ+
13. (r1/r(k1)) < (p[i + 1] - p[i])
14. j : ℕ||p||
15. (r(j)/r(||p|| * imax(k;k1))) < e
⊢ (r(j)/r(||p|| * imax(k;k1))) < (p[i + 1] - p[i])

---

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.  i  :  \mBbbN{}||p||  -  1
11.  p[i]  <  p[i  +  1]
12.  k1  :  \mBbbN{}\msupplus{}
13.  (r1/r(k1))  <  (p[i  +  1]  -  p[i])
\mvdash{}  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}j:\mBbbN{}||p||.  (((r(j)/r(N))  <  e)  \mwedge{}  ((r(j)/r(N))  <  (p[i  +  1]  -  p[i])))


By

---

Latex:
(D  0  With  \mkleeneopen{}||p||  *  imax(k;k1)\mkleeneclose{}    THEN  Auto)

---

Home Index