---

Step * 1 1 of Lemma nearby-partition-sum


1. I : Interval
2. icompact(I)
3. iproper(I)
4. f : I ⟶ℝ
5. mc : f[x] continuous for x ∈ I
6. ∀m,n:ℕ+.
     (mc m n ∈ {d:ℝ| (r0 < d) ∧ (∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n)))))} )
7. p : partition(I)
8. x : partition-choice(full-partition(I;p))
9. alpha : {a:ℝ| r0 < a} 
10. ||full-partition(I;p)|| = (||p|| + 2) ∈ ℤ
11. r0 < r(2 * (||p|| + 1))
12. r0 < |I|
⊢ ∃e:{e:ℝ| r0 < e} 
   ∀q:partition(I). ∀y:partition-choice(full-partition(I;q)).
     (nearby-partitions(e;p;q)
     ⇒ (∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e))
     ⇒ (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ alpha))
BY
{ ((Assert r0 < (r(2 * (||p|| + 1)) * |I|) BY
          EAuto 1)
   THEN (InstLemma `small-reciprocal-real-ext`
          [⌜(alpha/r(2 * (||p|| + 1)) * |I|)⌝]⋅
         THENA (MemTypeCD
                THEN Auto
                THEN MoveToConcl (-1)
                THEN (GenConclTerm ⌜r(2 * (||p|| + 1)) * |I|⌝⋅ THENA Auto)
                THEN All Thin
                THEN Auto
                THEN nRMul ⌜v⌝ 0⋅
                THEN Auto)
         )
   ) }

1
1. I : Interval
2. icompact(I)
3. iproper(I)
4. f : I ⟶ℝ
5. mc : f[x] continuous for x ∈ I
6. ∀m,n:ℕ+.
     (mc m n ∈ {d:ℝ| (r0 < d) ∧ (∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n)))))} )
7. p : partition(I)
8. x : partition-choice(full-partition(I;p))
9. alpha : {a:ℝ| r0 < a} 
10. ||full-partition(I;p)|| = (||p|| + 2) ∈ ℤ
11. r0 < r(2 * (||p|| + 1))
12. r0 < |I|
13. r0 < (r(2 * (||p|| + 1)) * |I|)
14. ∃k:ℕ+. ((r1/r(k)) < (alpha/r(2 * (||p|| + 1)) * |I|))
⊢ ∃e:{e:ℝ| r0 < e} 
   ∀q:partition(I). ∀y:partition-choice(full-partition(I;q)).
     (nearby-partitions(e;p;q)
     ⇒ (∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e))
     ⇒ (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ alpha))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  iproper(I)
4.  f  :  I  {}\mrightarrow{}\mBbbR{}
5.  mc  :  f[x]  continuous  for  x  \mmember{}  I
6.  \mforall{}m,n:\mBbbN{}\msupplus{}.
          (mc  m  n  \mmember{}  \{d:\mBbbR{}| 
                                (r0  <  d)
                                \mwedge{}  (\mforall{}x,y:\mBbbR{}.    ((x  \mmember{}  I)  {}\mRightarrow{}  (y  \mmember{}  I)  {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(n)))))\}  )
7.  p  :  partition(I)
8.  x  :  partition-choice(full-partition(I;p))
9.  alpha  :  \{a:\mBbbR{}|  r0  <  a\} 
10.  ||full-partition(I;p)||  =  (||p||  +  2)
11.  r0  <  r(2  *  (||p||  +  1))
12.  r0  <  |I|
\mvdash{}  \mexists{}e:\{e:\mBbbR{}|  r0  <  e\} 
      \mforall{}q:partition(I).  \mforall{}y:partition-choice(full-partition(I;q)).
          (nearby-partitions(e;p;q)
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||p||  +  1.  (|x[i]  -  y[i]|  \mleq{}  e))
          {}\mRightarrow{}  (|S(f;full-partition(I;q))  -  S(f;full-partition(I;p))|  \mleq{}  alpha))


By

---

Latex:
((Assert  r0  <  (r(2  *  (||p||  +  1))  *  |I|)  BY
                EAuto  1)
  THEN  (InstLemma  `small-reciprocal-real-ext`
                [\mkleeneopen{}(alpha/r(2  *  (||p||  +  1))  *  |I|)\mkleeneclose{}]\mcdot{}
              THENA  (MemTypeCD
                            THEN  Auto
                            THEN  MoveToConcl  (-1)
                            THEN  (GenConclTerm  \mkleeneopen{}r(2  *  (||p||  +  1))  *  |I|\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  All  Thin
                            THEN  Auto
                            THEN  nRMul  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{}
                            THEN  Auto)
              )
  )

---

Home Index