---

Step * of Lemma series-converges-rmul-ext

∀c:ℝ. ∀x:ℕ ⟶ ℝ.  (Σn.x[n]↓ ⇒ Σn.x[n] * c↓)
BY
{ Extract of Obid: series-converges-rmul
  not unfolding  absval rsum rmul canonical-bound
  finishing with Auto
  normalizes to:
  
  λc,x,cnvg. let a,mdlus = cnvg in <a * c, λk.eval m = canonical-bound(λn.|c n|) in mdlus (m * k)> }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  series-converges-rmul
not  unfolding    absval  rsum  rmul  canonical-bound
finishing  with  Auto
normalizes  to:

\mlambda{}c,x,cnvg.  let  a,mdlus  =  cnvg  in  <a  *  c,  \mlambda{}k.eval  m  =  canonical-bound(\mlambda{}n.|c  n|)  in  mdlus  (m  *  k)>

---

Home Index