---

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


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. x : ℕ||p|| - 1
11. p[x] < p[x + 1]
12. k1 : ℕ+
13. (r1/r(k1)) < (p[x + 1] - p[x])
14. N : ℕ+
15. ∀j:ℕ||p||. (((r(j)/r(N)) < e) ∧ ((r(j)/r(N)) < (p[x + 1] - p[x])))
16. i : ℕ||mklist(||p||;λj.if x <z j then p[j] - (r(||p|| - 1 - j)/r(N)) else p[j] + (r(j)/r(N)) fi )||
17. j : ℕ||p||
18. i < j
19. p[i] ≤ p[j]
⊢ if x <z i then p[i] - (r(||p|| - 1 - i)/r(N)) else p[i] + (r(i)/r(N)) fi  < if x <z j
then p[j] - (r(||p|| - 1 - j)/r(N))
else p[j] + (r(j)/r(N))
fi 
BY
{ ((BoolCase ⌜x <z i⌝⋅ THENA Auto) THEN (BoolCase ⌜x <z j⌝⋅ 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. x : ℕ||p|| - 1
11. p[x] < p[x + 1]
12. k1 : ℕ+
13. (r1/r(k1)) < (p[x + 1] - p[x])
14. N : ℕ+
15. ∀j:ℕ||p||. (((r(j)/r(N)) < e) ∧ ((r(j)/r(N)) < (p[x + 1] - p[x])))
16. i : ℕ||mklist(||p||;λj.if x <z j then p[j] - (r(||p|| - 1 - j)/r(N)) else p[j] + (r(j)/r(N)) fi )||
17. j : ℕ||p||
18. i < j
19. p[i] ≤ p[j]
20. x < i
21. x < j
⊢ (p[i] - (r(||p|| - 1 - i)/r(N))) < (p[j] - (r(||p|| - 1 - j)/r(N)))

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. x : ℕ||p|| - 1
11. p[x] < p[x + 1]
12. k1 : ℕ+
13. (r1/r(k1)) < (p[x + 1] - p[x])
14. N : ℕ+
15. ∀j:ℕ||p||. (((r(j)/r(N)) < e) ∧ ((r(j)/r(N)) < (p[x + 1] - p[x])))
16. i : ℕ||mklist(||p||;λj.if x <z j then p[j] - (r(||p|| - 1 - j)/r(N)) else p[j] + (r(j)/r(N)) fi )||
17. ¬x < i
18. j : ℕ||p||
19. i < j
20. p[i] ≤ p[j]
21. x < j
⊢ (p[i] + (r(i)/r(N))) < (p[j] - (r(||p|| - 1 - j)/r(N)))

3
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. x : ℕ||p|| - 1
11. p[x] < p[x + 1]
12. k1 : ℕ+
13. (r1/r(k1)) < (p[x + 1] - p[x])
14. N : ℕ+
15. ∀j:ℕ||p||. (((r(j)/r(N)) < e) ∧ ((r(j)/r(N)) < (p[x + 1] - p[x])))
16. i : ℕ||mklist(||p||;λj.if x <z j then p[j] - (r(||p|| - 1 - j)/r(N)) else p[j] + (r(j)/r(N)) fi )||
17. ¬x < i
18. j : ℕ||p||
19. ¬x < j
20. i < j
21. p[i] ≤ p[j]
⊢ (p[i] + (r(i)/r(N))) < (p[j] + (r(j)/r(N)))

---

Latex:

---

Latex:

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.  x  :  \mBbbN{}||p||  -  1
11.  p[x]  <  p[x  +  1]
12.  k1  :  \mBbbN{}\msupplus{}
13.  (r1/r(k1))  <  (p[x  +  1]  -  p[x])
14.  N  :  \mBbbN{}\msupplus{}
15.  \mforall{}j:\mBbbN{}||p||.  (((r(j)/r(N))  <  e)  \mwedge{}  ((r(j)/r(N))  <  (p[x  +  1]  -  p[x])))
16.  i  :  \mBbbN{}||mklist(||p||;\mlambda{}j.if  x  <z  j
                                                      then  p[j]  -  (r(||p||  -  1  -  j)/r(N))
                                                      else  p[j]  +  (r(j)/r(N))
                                                      fi  )||
17.  j  :  \mBbbN{}||p||
18.  i  <  j
19.  p[i]  \mleq{}  p[j]
\mvdash{}  if  x  <z  i  then  p[i]  -  (r(||p||  -  1  -  i)/r(N))  else  p[i]  +  (r(i)/r(N))  fi    <  if  x  <z  j
then  p[j]  -  (r(||p||  -  1  -  j)/r(N))
else  p[j]  +  (r(j)/r(N))
fi 


By

---

Latex:
((BoolCase  \mkleeneopen{}x  <z  i\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (BoolCase  \mkleeneopen{}x  <z  j\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index