---

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


1. I : Interval
2. icompact(I)
3. e : {e:ℝ| r0 < e} 
4. k : ℕ+
5. (r1/r(k)) < e
6. left-endpoint(I) < right-endpoint(I)
7. u : ℝ
8. v : ℝ List
9. ¬(v = [] ∈ (ℝ List))
10. ¬([u / v] = [] ∈ (ℝ List))
11. frs-non-dec([u / v]) ∧ (0 < ||[u / v]|| ⇒ ((left-endpoint(I) ≤ [u / v][0]) ∧ (last([u / v]) ≤ right-endpoint(I))))
⊢ frs-non-dec(v) ∧ (0 < ||v|| ⇒ ((left-endpoint(I) ≤ v[0]) ∧ (last(v) ≤ right-endpoint(I))))
BY
{ (RepeatFor 2 (D -1) THEN Auto) }

1
1. I : Interval
2. icompact(I)
3. e : {e:ℝ| r0 < e} 
4. k : ℕ+
5. (r1/r(k)) < e
6. left-endpoint(I) < right-endpoint(I)
7. u : ℝ
8. v : ℝ List
9. ¬(v = [] ∈ (ℝ List))
10. ¬([u / v] = [] ∈ (ℝ List))
11. frs-non-dec([u / v])
12. left-endpoint(I) ≤ [u / v][0]
13. last([u / v]) ≤ right-endpoint(I)
⊢ frs-non-dec(v)

2
1. I : Interval
2. icompact(I)
3. e : {e:ℝ| r0 < e} 
4. k : ℕ+
5. (r1/r(k)) < e
6. left-endpoint(I) < right-endpoint(I)
7. u : ℝ
8. v : ℝ List
9. ¬(v = [] ∈ (ℝ List))
10. ¬([u / v] = [] ∈ (ℝ List))
11. frs-non-dec([u / v])
12. left-endpoint(I) ≤ [u / v][0]
13. last([u / v]) ≤ right-endpoint(I)
14. frs-non-dec(v)
15. 0 < ||v||
⊢ left-endpoint(I) ≤ v[0]

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
4.  k  :  \mBbbN{}\msupplus{}
5.  (r1/r(k))  <  e
6.  left-endpoint(I)  <  right-endpoint(I)
7.  u  :  \mBbbR{}
8.  v  :  \mBbbR{}  List
9.  \mneg{}(v  =  [])
10.  \mneg{}([u  /  v]  =  [])
11.  frs-non-dec([u  /  v])
\mwedge{}  (0  <  ||[u  /  v]||  {}\mRightarrow{}  ((left-endpoint(I)  \mleq{}  [u  /  v][0])  \mwedge{}  (last([u  /  v])  \mleq{}  right-endpoint(I))))
\mvdash{}  frs-non-dec(v)  \mwedge{}  (0  <  ||v||  {}\mRightarrow{}  ((left-endpoint(I)  \mleq{}  v[0])  \mwedge{}  (last(v)  \mleq{}  right-endpoint(I))))


By

---

Latex:
(RepeatFor  2  (D  -1)  THEN  Auto)

---

Home Index