---

Step * of Lemma nearby-increasing-partition-avoids

∀I:Interval
  ((icompact(I) ∧ iproper(I))
  ⇒ (∀p:partition(I)
        (frs-increasing(p)
        ⇒ (∀L:ℝ List. ∀e:{e:ℝ| r0 < e} .
              ∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;p;q) ∧ frs-separated(q;L))))))
BY
{ ((Auto THEN DVar `p')
   THEN (Assert partitions(I;p) BY
               (Unhide THEN Auto))
   THEN Thin 5
   THEN MoveToConcl (-1)
   THEN MoveToConcl (-3)
   THEN MoveToConcl (-1)
   THEN ListInd (-2)
   THEN Auto) }

1
1. I : Interval
2. icompact(I)
3. iproper(I)
4. L : ℝ List
5. e : {e:ℝ| r0 < e} 
6. frs-increasing([])
7. partitions(I;[])
⊢ ∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;[];q) ∧ frs-separated(q;L))

2
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])
⊢ ∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;[u / v];q) ∧ frs-separated(q;L))

---

Latex:

---

Latex:
\mforall{}I:Interval
    ((icompact(I)  \mwedge{}  iproper(I))
    {}\mRightarrow{}  (\mforall{}p:partition(I)
                (frs-increasing(p)
                {}\mRightarrow{}  (\mforall{}L:\mBbbR{}  List.  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
                            \mexists{}q:partition(I)
                              (frs-increasing(q)  \mwedge{}  nearby-partitions(e;p;q)  \mwedge{}  frs-separated(q;L))))))


By

---

Latex:
((Auto  THEN  DVar  `p')
  THEN  (Assert  partitions(I;p)  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  5
  THEN  MoveToConcl  (-1)
  THEN  MoveToConcl  (-3)
  THEN  MoveToConcl  (-1)
  THEN  ListInd  (-2)
  THEN  Auto)

---

Home Index