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