---

Step * 1 2 1 2 1 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. left-endpoint(I) < p[0]
11. k1 : ℕ+
12. (r1/r(k1)) < (p[0] - left-endpoint(I))
13. i : ℕ||p||
14. (r(i)/r(||p|| * imax(k;k1))) < e
⊢ (r(i)/r(||p|| * imax(k;k1))) ≤ (r1/r(k1))
BY
{ ((Assert (r1/r(imax(k;k1))) ≤ (r1/r(k1)) BY
          ((Assert k1 ≤ imax(k;k1) BY Auto) THEN Auto))
   THEN (RWO "-1<" 0 THENA Auto)
   THEN (GenConcl ⌜imax(k;k1) = N ∈ ℕ+⌝⋅ 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. left-endpoint(I) < p[0]
11. k1 : ℕ+
12. (r1/r(k1)) < (p[0] - left-endpoint(I))
13. i : ℕ||p||
14. (r(i)/r(||p|| * imax(k;k1))) < e
15. (r1/r(imax(k;k1))) ≤ (r1/r(k1))
16. N : ℕ+
17. imax(k;k1) = N ∈ ℕ+
⊢ (r(i)/r(||p|| * N)) ≤ (r1/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.  left-endpoint(I)  <  p[0]
11.  k1  :  \mBbbN{}\msupplus{}
12.  (r1/r(k1))  <  (p[0]  -  left-endpoint(I))
13.  i  :  \mBbbN{}||p||
14.  (r(i)/r(||p||  *  imax(k;k1)))  <  e
\mvdash{}  (r(i)/r(||p||  *  imax(k;k1)))  \mleq{}  (r1/r(k1))


By

---

Latex:
((Assert  (r1/r(imax(k;k1)))  \mleq{}  (r1/r(k1))  BY
                ((Assert  k1  \mleq{}  imax(k;k1)  BY  Auto)  THEN  Auto))
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}imax(k;k1)  =  N\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index