---

Step * of Lemma comparison-test-ext

∀y:ℕ ⟶ ℝ. (Σn.y[n]↓ ⇒ (∀x:ℕ ⟶ ℝ. Σn.x[n]↓ supposing ∀n:ℕ. (|x[n]| ≤ y[n])))
BY
{ Extract of Obid: comparison-test
  not unfolding  divide rsum
  finishing with Auto
  normalizes to:
  
  λy,converges,x. <λn.eval m = 4 * n in
                      (Σ{x i | 0≤i≤let y,c = converges in c (2 * m)} m) ÷ 4
                  , λk.let y,c = converges 
                       in (c (2 * 4 * k)) + 1
                  > }

---

Latex:

---

Latex:
\mforall{}y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  (\mSigma{}n.y[n]\mdownarrow{}  {}\mRightarrow{}  (\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mSigma{}n.x[n]\mdownarrow{}  supposing  \mforall{}n:\mBbbN{}.  (|x[n]|  \mleq{}  y[n])))


By

---

Latex:
Extract  of  Obid:  comparison-test
not  unfolding    divide  rsum
finishing  with  Auto
normalizes  to:

\mlambda{}y,converges,x.  <\mlambda{}n.eval  m  =  4  *  n  in
                                        (\mSigma{}\{x  i  |  0\mleq{}i\mleq{}let  y,c  =  converges  in  c  (2  *  m)\}  m)  \mdiv{}  4
                                ,  \mlambda{}k.let  y,c  =  converges 
                                          in  (c  (2  *  4  *  k))  +  1
                                >

---

Home Index