---

Step * of Lemma series-converges-tail2-ext

∀N:ℕ. ∀x:ℕ ⟶ ℝ.  (Σn.x[n + N]↓ ⇒ Σn.x[n]↓)
BY
{ xxxExtract of Obid: series-converges-tail2
     not unfolding  rsum radd
     finishing with Auto
     normalizes to:
     
     λN,x,converges. let a,f = converges in <a + Σ{x n | 0≤n≤N - 1}, λk.(N + (f k))>xxx }

---

Latex:

---

Latex:
\mforall{}N:\mBbbN{}.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.    (\mSigma{}n.x[n  +  N]\mdownarrow{}  {}\mRightarrow{}  \mSigma{}n.x[n]\mdownarrow{})


By

---

Latex:
xxxExtract  of  Obid:  series-converges-tail2
      not  unfolding    rsum  radd
      finishing  with  Auto
      normalizes  to:
     
      \mlambda{}N,x,converges.  let  a,f  =  converges  in  <a  +  \mSigma{}\{x  n  |  0\mleq{}n\mleq{}N  -  1\},  \mlambda{}k.(N  +  (f  k))>xxx

---

Home Index