---

Step * of Lemma rexp-approx-for-small-ext

∀N:ℕ+. ∀x:{x:ℝ| |x| ≤ (r1/r(4))} .  (∃z:ℤ [(|e^x - (r(z)/r(2 * N))| ≤ (r(2)/r(N)))])
BY
{ Extract of Obid: rexp-approx-for-small
  not unfolding  rexp-approx genfact-inv
  finishing with Auto
  normalizes to:
  
  λN,x. rexp-approx(x;genfact-inv(N;3;m.4 * m);N) }

---

Latex:

---

Latex:
\mforall{}N:\mBbbN{}\msupplus{}.  \mforall{}x:\{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(4))\}  .    (\mexists{}z:\mBbbZ{}  [(|e\^{}x  -  (r(z)/r(2  *  N))|  \mleq{}  (r(2)/r(N)))])


By

---

Latex:
Extract  of  Obid:  rexp-approx-for-small
not  unfolding    rexp-approx  genfact-inv
finishing  with  Auto
normalizes  to:

\mlambda{}N,x.  rexp-approx(x;genfact-inv(N;3;m.4  *  m);N)

---

Home Index