Step * of Lemma converges-to-rexp-ext

x:ℝlim n→∞.approx-rexp(x;n) e^x
BY
Extract of Obid: converges-to-rexp
  not unfolding  divide fastexp
  finishing with Auto
  normalizes to:
  
  λx,k. (k (k ÷ if ((((x 1) 1) ÷ 2) 1) < (0)  then 1  else 3^(((x 1) 1) ÷ 2) 1) 1) }


Latex:


Latex:
\mforall{}x:\mBbbR{}.  lim  n\mrightarrow{}\minfty{}.approx-rexp(x;n)  =  e\^{}x


By


Latex:
Extract  of  Obid:  converges-to-rexp
not  unfolding    divide  fastexp
finishing  with  Auto
normalizes  to:

\mlambda{}x,k.  (k  +  (k  \mdiv{}  if  ((((x  1)  +  1)  \mdiv{}  2)  +  1)  <  (0)    then  1    else  3\^{}(((x  1)  +  1)  \mdiv{}  2)  +  1)  +  1)




Home Index