---

Step * of Lemma nearby-partition-choice

∀I:Interval
  (icompact(I)
  ⇒ (∀p,q:partition(I). ∀e:{e:ℝ| r0 < e} .
        (nearby-partitions(e;p;q)
        ⇒ (∀x:partition-choice(full-partition(I;p))
              ∃y:partition-choice(full-partition(I;q)). ∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e)))))
BY
{ Auto }

1
1. I : Interval@i
2. icompact(I)
3. p : partition(I)@i
4. q : partition(I)@i
5. e : {e:ℝ| r0 < e} @i
6. nearby-partitions(e;p;q)
7. x : partition-choice(full-partition(I;p))@i
⊢ ∃y:partition-choice(full-partition(I;q)). ∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e)

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}p,q:partition(I).  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
                (nearby-partitions(e;p;q)
                {}\mRightarrow{}  (\mforall{}x:partition-choice(full-partition(I;p))
                            \mexists{}y:partition-choice(full-partition(I;q)).  \mforall{}i:\mBbbN{}||p||  +  1.  (|x[i]  -  y[i]|  \mleq{}  e)))))


By

---

Latex:
Auto

---

Home Index