Step * 1 of Lemma continuous-range-totally-bounded


1. : ℕ+
2. : ℝ
3. r0 < e
4. : ℕ+
5. (r1/r(k)) < e
6. : ℝ
7. Interval
8. icompact(I)
9. I ⟶ℝ
10. r0 < d
11. ∀x,y:ℝ.  ((x ∈ I)  (y ∈ I)  (|x y| ≤ d)  (|f[x] f[y]| ≤ (r1/r(k))))
⊢ ∃n:ℕ+. ∃a:ℕn ⟶ ℝ((∀i:ℕn. (a i ∈ f[x](x∈I))) ∧ (∀x:ℝ((x ∈ f[x](x∈I))  (∃i:ℕn. (|x i| < e)))))
BY
((InstLemma `partition-exists` [⌜I⌝; ⌜d⌝])⋅
   THEN Auto
   THEN ExRepD
   THEN InstConcl [⌜||full-partition(I;p)||⌝;⌜λi.f(full-partition(I;p)[i])⌝]⋅
   THEN Auto)⋅ }

1
.....wf..... 
1. : ℕ+
2. : ℝ
3. r0 < e
4. : ℕ+
5. (r1/r(k)) < e
6. : ℝ
7. Interval
8. icompact(I)
9. I ⟶ℝ
10. r0 < d
11. ∀x,y:ℝ.  ((x ∈ I)  (y ∈ I)  (|x y| ≤ d)  (|f[x] f[y]| ≤ (r1/r(k))))
12. partition(I)
13. partition-mesh(I;p) ≤ d
⊢ ||full-partition(I;p)|| ∈ ℕ+

2
1. : ℕ+
2. : ℝ
3. r0 < e
4. : ℕ+
5. (r1/r(k)) < e
6. : ℝ
7. Interval
8. icompact(I)
9. I ⟶ℝ
10. r0 < d
11. ∀x,y:ℝ.  ((x ∈ I)  (y ∈ I)  (|x y| ≤ d)  (|f[x] f[y]| ≤ (r1/r(k))))
12. partition(I)
13. partition-mesh(I;p) ≤ d
14. : ℕ||full-partition(I;p)||
⊢ full-partition(I;p)[i] ∈ I

3
1. : ℕ+
2. : ℝ
3. r0 < e
4. : ℕ+
5. (r1/r(k)) < e
6. : ℝ
7. Interval
8. icompact(I)
9. I ⟶ℝ
10. r0 < d
11. ∀x,y:ℝ.  ((x ∈ I)  (y ∈ I)  (|x y| ≤ d)  (|f[x] f[y]| ≤ (r1/r(k))))
12. partition(I)
13. partition-mesh(I;p) ≤ d
14. : ℕ||full-partition(I;p)||
⊢ i.f(full-partition(I;p)[i])) i ∈ f[x](x∈I)

4
1. : ℕ+
2. : ℝ
3. r0 < e
4. : ℕ+
5. (r1/r(k)) < e
6. : ℝ
7. Interval
8. icompact(I)
9. I ⟶ℝ
10. r0 < d
11. ∀x,y:ℝ.  ((x ∈ I)  (y ∈ I)  (|x y| ≤ d)  (|f[x] f[y]| ≤ (r1/r(k))))
12. partition(I)
13. partition-mesh(I;p) ≤ d
14. ∀i:ℕ||full-partition(I;p)||. ((λi.f(full-partition(I;p)[i])) i ∈ f[x](x∈I))
15. : ℝ
16. x ∈ f[x](x∈I)
⊢ ∃i:ℕ||full-partition(I;p)||. (|x i.f(full-partition(I;p)[i])) i| < e)


Latex:


Latex:

1.  m  :  \mBbbN{}\msupplus{}
2.  e  :  \mBbbR{}
3.  r0  <  e
4.  k  :  \mBbbN{}\msupplus{}
5.  (r1/r(k))  <  e
6.  d  :  \mBbbR{}
7.  I  :  Interval
8.  icompact(I)
9.  f  :  I  {}\mrightarrow{}\mBbbR{}
10.  r0  <  d
11.  \mforall{}x,y:\mBbbR{}.    ((x  \mmember{}  I)  {}\mRightarrow{}  (y  \mmember{}  I)  {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(k))))
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}
      \mexists{}a:\mBbbN{}n  {}\mrightarrow{}  \mBbbR{}.  ((\mforall{}i:\mBbbN{}n.  (a  i  \mmember{}  f[x](x\mmember{}I)))  \mwedge{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  f[x](x\mmember{}I))  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}n.  (|x  -  a  i|  <  e)))))


By


Latex:
((InstLemma  `partition-exists`  [\mkleeneopen{}I\mkleeneclose{};  \mkleeneopen{}d\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}||full-partition(I;p)||\mkleeneclose{};\mkleeneopen{}\mlambda{}i.f(full-partition(I;p)[i])\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}




Home Index