---

Step * 1 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|
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))
BY
{ (InstLemma `Inorm-non-neg` [⌜I⌝;⌜f⌝;⌜mc⌝]⋅ THENA 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|))
15. r0 ≤ ||f[x]||_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|
13.  r0  <  (r(2  *  (||p||  +  1))  *  |I|)
14.  \mexists{}k:\mBbbN{}\msupplus{}.  ((r1/r(k))  <  (alpha/r(2  *  (||p||  +  1))  *  |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:
(InstLemma  `Inorm-non-neg`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index