---

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


1. I : Interval
2. icompact(I)
3. iproper(I)
4. L : ℝ List
5. u : ℝ
6. v : ℝ List
7. ∀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))))
8. e : {e:ℝ| r0 < e} 
9. frs-increasing([u / v])
10. partitions(I;[u / v])
11. frs-increasing(v)
⊢ ∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;[u / v];q) ∧ frs-separated(q;L))
BY
{ (Assert partitions(I;v) BY
         (ParallelOp -2
          THEN Auto
          THEN Try ((BLemma `frs-increasing-non-dec` THEN Auto))
          THEN (Assert 0 < ||[u / v]|| BY
                      Auto)
          THEN ThinTrivial
          THEN D (-1)
          THEN Reduce -2
          THEN RWO "last_cons" (-1)
          THEN Auto
          THEN (D -7 With ⌜0⌝  THENA Auto)
          THEN (InstHyp [⌜1⌝] (-1)⋅ THENA Auto)
          THEN Reduce -1
          THEN Auto)) }

1
1. I : Interval
2. icompact(I)
3. iproper(I)
4. L : ℝ List
5. u : ℝ
6. v : ℝ List
7. ∀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))))
8. e : {e:ℝ| r0 < e} 
9. frs-increasing([u / v])
10. partitions(I;[u / v])
11. frs-increasing(v)
12. partitions(I;v)
⊢ ∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;[u / v];q) ∧ frs-separated(q;L))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  iproper(I)
4.  L  :  \mBbbR{}  List
5.  u  :  \mBbbR{}
6.  v  :  \mBbbR{}  List
7.  \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))))
8.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
9.  frs-increasing([u  /  v])
10.  partitions(I;[u  /  v])
11.  frs-increasing(v)
\mvdash{}  \mexists{}q:partition(I).  (frs-increasing(q)  \mwedge{}  nearby-partitions(e;[u  /  v];q)  \mwedge{}  frs-separated(q;L))


By

---

Latex:
(Assert  partitions(I;v)  BY
              (ParallelOp  -2
                THEN  Auto
                THEN  Try  ((BLemma  `frs-increasing-non-dec`  THEN  Auto))
                THEN  (Assert  0  <  ||[u  /  v]||  BY
                                        Auto)
                THEN  ThinTrivial
                THEN  D  (-1)
                THEN  Reduce  -2
                THEN  RWO  "last\_cons"  (-1)
                THEN  Auto
                THEN  (D  -7  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  Reduce  -1
                THEN  Auto))

---

Home Index