---

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

.....wf..... 
1. I : Interval
2. icompact(I)
3. iproper(I)
4. L : ℝ List
5. u : ℝ
6. v : ℝ List
7. ¬(v = [] ∈ (ℝ List))
8. ∀e:{e:ℝ| r0 < e} 
     (frs-increasing(v)
     ⇒ partitions(I;v)
     ⇒ (∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;v;q) ∧ frs-separated(q;L))))
9. e : {e:ℝ| r0 < e} 
10. frs-increasing([u / v])
11. partitions(I;[u / v])
12. frs-increasing(v)
13. partitions(I;v)
14. 0 < ||v||
15. r0 < (v[0] - u)
16. r0 < rmin(e;(v[0] - u/r(3)))
17. q : partition(I)
18. frs-increasing(q)
19. nearby-partitions(rmin(e;(v[0] - u/r(3)));v;q)
20. frs-separated(q;L)
21. c : ℝ
22. u ≤ c
23. c < (u + rmin(e;(v[0] - u/r(3))))
24. (∀x∈L.c ≠ x)
25. frs-increasing([c / q])
⊢ [c / q] ∈ partition(I)
BY
{ ((Assert partitions(I;q) BY
          (DVar `q' THEN Unhide THEN Auto))
   THEN (MemTypeCD THEN Auto)
   THEN D 0
   THEN Try ((BLemma `frs-increasing-non-dec` THEN Auto))
   THEN Reduce 0
   THEN (Assert ||v|| = ||q|| ∈ ℤ BY
               Auto)
   THEN RWO "last_cons" 0
   THEN Auto) }

1
1. I : Interval
2. icompact(I)
3. iproper(I)
4. L : ℝ List
5. u : ℝ
6. v : ℝ List
7. ¬(v = [] ∈ (ℝ List))
8. ∀e:{e:ℝ| r0 < e} 
     (frs-increasing(v)
     ⇒ partitions(I;v)
     ⇒ (∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;v;q) ∧ frs-separated(q;L))))
9. e : {e:ℝ| r0 < e} 
10. frs-increasing([u / v])
11. partitions(I;[u / v])
12. frs-increasing(v)
13. partitions(I;v)
14. 0 < ||v||
15. r0 < (v[0] - u)
16. r0 < rmin(e;(v[0] - u/r(3)))
17. q : partition(I)
18. frs-increasing(q)
19. nearby-partitions(rmin(e;(v[0] - u/r(3)));v;q)
20. frs-separated(q;L)
21. c : ℝ
22. u ≤ c
23. c < (u + rmin(e;(v[0] - u/r(3))))
24. (∀x∈L.c ≠ x)
25. frs-increasing([c / q])
26. partitions(I;q)
27. ||v|| = ||q|| ∈ ℤ
28. 0 < ||q|| + 1
⊢ left-endpoint(I) ≤ c

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  Interval
2.  icompact(I)
3.  iproper(I)
4.  L  :  \mBbbR{}  List
5.  u  :  \mBbbR{}
6.  v  :  \mBbbR{}  List
7.  \mneg{}(v  =  [])
8.  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\} 
          (frs-increasing(v)
          {}\mRightarrow{}  partitions(I;v)
          {}\mRightarrow{}  (\mexists{}q:partition(I).  (frs-increasing(q)  \mwedge{}  nearby-partitions(e;v;q)  \mwedge{}  frs-separated(q;L))))
9.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
10.  frs-increasing([u  /  v])
11.  partitions(I;[u  /  v])
12.  frs-increasing(v)
13.  partitions(I;v)
14.  0  <  ||v||
15.  r0  <  (v[0]  -  u)
16.  r0  <  rmin(e;(v[0]  -  u/r(3)))
17.  q  :  partition(I)
18.  frs-increasing(q)
19.  nearby-partitions(rmin(e;(v[0]  -  u/r(3)));v;q)
20.  frs-separated(q;L)
21.  c  :  \mBbbR{}
22.  u  \mleq{}  c
23.  c  <  (u  +  rmin(e;(v[0]  -  u/r(3))))
24.  (\mforall{}x\mmember{}L.c  \mneq{}  x)
25.  frs-increasing([c  /  q])
\mvdash{}  [c  /  q]  \mmember{}  partition(I)


By

---

Latex:
((Assert  partitions(I;q)  BY
                (DVar  `q'  THEN  Unhide  THEN  Auto))
  THEN  (MemTypeCD  THEN  Auto)
  THEN  D  0
  THEN  Try  ((BLemma  `frs-increasing-non-dec`  THEN  Auto))
  THEN  Reduce  0
  THEN  (Assert  ||v||  =  ||q||  BY
                          Auto)
  THEN  RWO  "last\_cons"  0
  THEN  Auto)

---

Home Index