---

Step * 1 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)
⊢ (left-endpoint(I) < p[0]) ∨ (last(p) < right-endpoint(I)) ∨ (∃i:ℕ||p|| - 1. (p[i] < p[i + 1]))
BY
{ (ListInd 3 THEN Auto THEN Reduce 0) }

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)))
⇒ partitions(I;v)
⇒ ((left-endpoint(I) < v[0]) ∨ (last(v) < right-endpoint(I)) ∨ (∃i:ℕ||v|| - 1. (v[i] < v[i + 1])))
10. ¬([u / v] = [] ∈ (ℝ List))
11. partitions(I;[u / v])
⊢ (left-endpoint(I) < u) ∨ (last([u / v]) < right-endpoint(I)) ∨ (∃i:ℕ(||v|| + 1) - 1. ([u / v][i] < [u / v][i + 1]))

---

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)
\mvdash{}  (left-endpoint(I)  <  p[0])  \mvee{}  (last(p)  <  right-endpoint(I))  \mvee{}  (\mexists{}i:\mBbbN{}||p||  -  1.  (p[i]  <  p[i  +  1]))


By

---

Latex:
(ListInd  3  THEN  Auto  THEN  Reduce  0)

---

Home Index