---

Step * of Lemma nearby-increasing-partition

∀I:Interval
  ((icompact(I) ∧ iproper(I))
  ⇒ (∀p:partition(I). ∀e:{e:ℝ| r0 < e} .  ∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;p;q))))
BY
{ (Auto THEN (InstLemma `small-reciprocal-real` [⌜e⌝]⋅ THENA Auto) THEN ExRepD THEN DVar `p' THEN (D 3 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)
⊢ ∃q:partition(I). (frs-increasing(q) ∧ nearby-partitions(e;p;q))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `small-reciprocal-real`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  DVar  `p'
  THEN  (D  3  THENA  Auto))

---

Home Index