---

Step * 1 of Lemma nearby-separated-partitions


1. I : Interval@i
2. icompact(I)
3. iproper(I)
4. p : partition(I)@i
5. q : partition(I)@i
6. e : {e:ℝ| r0 < e} @i
7. q1 : partition(I)
8. frs-increasing(q1)
9. nearby-partitions(e;p;q1)
⊢ ∃q':partition(I). (separated-partitions(q1;q') ∧ nearby-partitions(e;p;q1) ∧ nearby-partitions(e;q;q'))
BY
{ (Assert (e/r(2)) ∈ {e:ℝ| r0 < e}  BY
         (DVar `e'⋅ THEN MemTypeCD THEN Auto THEN nRMul ⌜r(2)⌝ 0⋅ THEN Auto)) }

1
1. I : Interval@i
2. icompact(I)
3. iproper(I)
4. p : partition(I)@i
5. q : partition(I)@i
6. e : {e:ℝ| r0 < e} @i
7. q1 : partition(I)
8. frs-increasing(q1)
9. nearby-partitions(e;p;q1)
10. (e/r(2)) ∈ {e:ℝ| r0 < e} 
⊢ ∃q':partition(I). (separated-partitions(q1;q') ∧ nearby-partitions(e;p;q1) ∧ nearby-partitions(e;q;q'))

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  icompact(I)
3.  iproper(I)
4.  p  :  partition(I)@i
5.  q  :  partition(I)@i
6.  e  :  \{e:\mBbbR{}|  r0  <  e\}  @i
7.  q1  :  partition(I)
8.  frs-increasing(q1)
9.  nearby-partitions(e;p;q1)
\mvdash{}  \mexists{}q':partition(I)
      (separated-partitions(q1;q')  \mwedge{}  nearby-partitions(e;p;q1)  \mwedge{}  nearby-partitions(e;q;q'))


By

---

Latex:
(Assert  (e/r(2))  \mmember{}  \{e:\mBbbR{}|  r0  <  e\}    BY
              (DVar  `e'\mcdot{}  THEN  MemTypeCD  THEN  Auto  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto))

---

Home Index