---

Step * 1 2 1 1 1 2 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. (¬(v = [] ∈ (ℝ List)))
⇒ partitions(I;v)
⇒ ((left-endpoint(I) < v[0]) ∨ (last(v) < right-endpoint(I)) ∨ (∃i:ℕ||v|| - 1. (v[i] < v[i + 1])))
11. ¬([u / v] = [] ∈ (ℝ List))
12. partitions(I;[u / v])
⊢ (left-endpoint(I) < u) ∨ (last(v) < right-endpoint(I)) ∨ (∃i:ℕ(||v|| + 1) - 1. ([u / v][i] < [u / v][i + 1]))
BY
{ (ThinTrivial THEN D -1) }

1
.....antecedent..... 
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. partitions(I;[u / v])
⊢ partitions(I;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. partitions(I;[u / v])
12. (left-endpoint(I) < v[0]) ∨ (last(v) < right-endpoint(I)) ∨ (∃i:ℕ||v|| - 1. (v[i] < v[i + 1]))
⊢ (left-endpoint(I) < u) ∨ (last(v) < right-endpoint(I)) ∨ (∃i:ℕ(||v|| + 1) - 1. ([u / v][i] < [u / v][i + 1]))

---

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{}(v  =  []))
{}\mRightarrow{}  partitions(I;v)
{}\mRightarrow{}  ((left-endpoint(I)  <  v[0])  \mvee{}  (last(v)  <  right-endpoint(I))  \mvee{}  (\mexists{}i:\mBbbN{}||v||  -  1.  (v[i]  <  v[i  +  1])))
11.  \mneg{}([u  /  v]  =  [])
12.  partitions(I;[u  /  v])
\mvdash{}  (left-endpoint(I)  <  u)
\mvee{}  (last(v)  <  right-endpoint(I))
\mvee{}  (\mexists{}i:\mBbbN{}(||v||  +  1)  -  1.  ([u  /  v][i]  <  [u  /  v][i  +  1]))


By

---

Latex:
(ThinTrivial  THEN  D  -1)

---

Home Index