---

Step * 1 of Lemma nearby-increasing-partition


1. I : Interval
2. icompact(I)
3. p : ℝ List
4. [%4] : partitions(I;p)
5. e : {e:ℝ| r0 < e} 
6. k : ℕ+
7. (r1/r(k)) < e
8. left-endpoint(I) < right-endpoint(I)
⊢ ∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;p;q))
BY
{ (BoolCase ⌜null(p)⌝⋅ THENA Auto) }

1
1. I : Interval
2. icompact(I)
3. p : ℝ List
4. [%4] : partitions(I;p)
5. e : {e:ℝ| r0 < e} 
6. k : ℕ+
7. (r1/r(k)) < e
8. left-endpoint(I) < right-endpoint(I)
9. p = [] ∈ (ℝ List)
⊢ ∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;p;q))

2
1. I : Interval
2. icompact(I)
3. p : ℝ List
4. ¬(p = [] ∈ (ℝ List))
5. [%4] : partitions(I;p)
6. e : {e:ℝ| r0 < e} 
7. k : ℕ+
8. (r1/r(k)) < e
9. left-endpoint(I) < right-endpoint(I)
⊢ ∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;p;q))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  p  :  \mBbbR{}  List
4.  [\%4]  :  partitions(I;p)
5.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
6.  k  :  \mBbbN{}\msupplus{}
7.  (r1/r(k))  <  e
8.  left-endpoint(I)  <  right-endpoint(I)
\mvdash{}  \mexists{}q:partition(I).  (frs-increasing(q)  \mwedge{}  nearby-partitions(e;p;q))


By

---

Latex:
(BoolCase  \mkleeneopen{}null(p)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index