---

Step * of Lemma nearby-separated-partitions

∀I:Interval
  ((icompact(I) ∧ iproper(I))
  ⇒ (∀p,q:partition(I). ∀e:{e:ℝ| r0 < e} .
        ∃p',q':partition(I). (separated-partitions(p';q') ∧ nearby-partitions(e;p;p') ∧ nearby-partitions(e;q;q'))))
BY
{ (Auto THEN (InstLemma `nearby-increasing-partition` [⌜I⌝;⌜p⌝;⌜e⌝]⋅ THENA Auto) THEN ParallelLast 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)
⊢ ∃q':partition(I). (separated-partitions(q1;q') ∧ nearby-partitions(e;p;q1) ∧ nearby-partitions(e;q;q'))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `nearby-increasing-partition`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto)

---

Home Index