---

Step * of Lemma partition-exists

∀I:Interval. (icompact(I) ⇒ (∀e:ℝ. ((r0 < e) ⇒ (∃p:partition(I). (partition-mesh(I;p) ≤ e)))))
BY
{ (Auto THEN ((FLemma `icompact-length-nonneg` [-3]) THENA Auto) THEN Assert ⌜∃k:ℕ+. ((|I|/e) ≤ r(k))⌝⋅) }

1
.....assertion..... 
1. I : Interval@i
2. icompact(I)@i
3. e : ℝ@i
4. r0 < e@i
5. r0 ≤ |I|
⊢ ∃k:ℕ+. ((|I|/e) ≤ r(k))

2
1. I : Interval@i
2. icompact(I)@i
3. e : ℝ@i
4. r0 < e@i
5. r0 ≤ |I|
6. ∃k:ℕ+. ((|I|/e) ≤ r(k))
⊢ ∃p:partition(I). (partition-mesh(I;p) ≤ e)

---

Latex:

---

Latex:
\mforall{}I:Interval.  (icompact(I)  {}\mRightarrow{}  (\mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}p:partition(I).  (partition-mesh(I;p)  \mleq{}  e)))))


By

---

Latex:
(Auto
  THEN  ((FLemma  `icompact-length-nonneg`  [-3])  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\mexists{}k:\mBbbN{}\msupplus{}.  ((|I|/e)  \mleq{}  r(k))\mkleeneclose{}\mcdot{})

---

Home Index