---

Step * of Lemma rnexp-converges-ext

∀x:ℝ. ((|x| < r1) ⇒ lim n→∞.x^n = r0)
BY
{ Extract of Obid: rnexp-converges
  not unfolding  absval exp-ratio rlessw int-to-real
  finishing with Auto
  normalizes to:
  
  λx,_. eval x1 = rlessw(λn.|x n|;r1) in λk.exp-ratio(|x x1| + (r1 x1);4 * x1;0;k;1) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  ((|x|  <  r1)  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x\^{}n  =  r0)


By

---

Latex:
Extract  of  Obid:  rnexp-converges
not  unfolding    absval  exp-ratio  rlessw  int-to-real
finishing  with  Auto
normalizes  to:

\mlambda{}x,$_{}$.  eval  x1  =  rlessw(\mlambda{}n.|x  n|;r1)  in  \mlambda{}k.exp-ratio(|x  x1|  +  (r1  x1);4  *  x1;\000C0;k;1)

---

Home Index