---

Step * of Lemma general-partition-sum-ext

∀I:Interval
  (icompact(I)
  ⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀e:{e:ℝ| r0 < e} .
        ∃d:{d:ℝ| r0 < d} 
         ∀p,q:{p:partition(I)| partition-mesh(I;p) ≤ d} . ∀x:partition-choice(full-partition(I;p)).
         ∀y:partition-choice(full-partition(I;q)).
           (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ (e * |I|))))
BY
{ Extract of Obid: general-partition-sum
  not unfolding  realops rlessw   
  finishing with Auto
  normalizes to:
  
  λI,_,_,mc,e. eval x = rlessw(r0;(e/r(2))) in <(mc 1 (x + 1)/r(2)), λp,q,x,y,n. <λv.Ax, Ax, Ax>> }

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  I.  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
                \mexists{}d:\{d:\mBbbR{}|  r0  <  d\} 
                  \mforall{}p,q:\{p:partition(I)|  partition-mesh(I;p)  \mleq{}  d\}  .  \mforall{}x:partition-choice(full-partition(I;p)).
                  \mforall{}y:partition-choice(full-partition(I;q)).
                      (|S(f;full-partition(I;q))  -  S(f;full-partition(I;p))|  \mleq{}  (e  *  |I|))))


By

---

Latex:
Extract  of  Obid:  general-partition-sum
not  unfolding    realops  rlessw     
finishing  with  Auto
normalizes  to:

\mlambda{}I,$_{}$,$_{}$,mc,e.  eval  x  =  rlessw(r0;(e/r(2)))  in  <(mc  1  \000C(x  +  1)/r(2)),  \mlambda{}p,q,x,y,n.  <\mlambda{}v.Ax,  Ax,  Ax>>

---

Home Index