---

Step * of Lemma nearby-partition-mesh

∀I:Interval
  (icompact(I)
  ⇒ (∀e:{e:ℝ| r0 < e} . ∀p,p':partition(I).
        (nearby-partitions((e/r(2));p;p') ⇒ (partition-mesh(I;p') ≤ (partition-mesh(I;p) + e)))))
BY
{ (Auto THEN Unfold `partition-mesh` 0) }

1
1. I : Interval
2. icompact(I)
3. e : {e:ℝ| r0 < e} 
4. p : partition(I)
5. p' : partition(I)
6. nearby-partitions((e/r(2));p;p')
⊢ frs-mesh(full-partition(I;p')) ≤ (frs-mesh(full-partition(I;p)) + e)

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .  \mforall{}p,p':partition(I).
                (nearby-partitions((e/r(2));p;p')  {}\mRightarrow{}  (partition-mesh(I;p')  \mleq{}  (partition-mesh(I;p)  +  e)))))


By

---

Latex:
(Auto  THEN  Unfold  `partition-mesh`  0)

---

Home Index