---

Step * of Lemma nearby-partition-sum-ext

∀I:Interval
  (icompact(I)
  ⇒ iproper(I)
  ⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀p:partition(I). ∀x:partition-choice(full-partition(I;p)).
      ∀alpha:{a:ℝ| r0 < a} .
        ∃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
{ Extract of Obid: nearby-partition-sum
  not unfolding  Inorm length  realops rlessw left-endpoint right-endpoint
  finishing with Auto
  normalizes to:
  
  λI,_,_,f,mc,p,_,alpha. eval x = rlessw(r0;(alpha/r(2 * (||p|| + 1)) * (right-endpoint(I) - left-endpoint(I)))) in
                         <rmin(mc 1 (x + 1);(alpha/r(4 * (||p|| + 1)) * (||f x||_I + r1))), λq,y,v,v,n. <λv.Ax, Ax, Ax>>\000C }

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  iproper(I)
    {}\mRightarrow{}  (\mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  I.  \mforall{}p:partition(I).
            \mforall{}x:partition-choice(full-partition(I;p)).  \mforall{}alpha:\{a:\mBbbR{}|  r0  <  a\}  .
                \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:
Extract  of  Obid:  nearby-partition-sum
not  unfolding    Inorm  length    realops  rlessw  left-endpoint  right-endpoint
finishing  with  Auto
normalizes  to:

\mlambda{}I,$_{}$,$_{}$,f,mc,p,$_{}$,alpha.  eval  \000Cx  =  rlessw(r0;(alpha/r(2  *  (||p||  +  1))
                                        *  (right-endpoint(I)  -  left-endpoint(I))))  in
                                        <rmin(mc  1  (x  +  1);(alpha/r(4  *  (||p||  +  1))  *  (||f  x||\_I  +  r1)))
                                        ,  \mlambda{}q,y,v,v,n.  <\mlambda{}v.Ax,  Ax,  Ax>
                                        >

---

Home Index