---

Step * of Lemma rational-approx-property-ext

∀x:ℝ. ∀n:ℕ+.  (|x - (x within 1/n)| ≤ (r1/r(n)))
BY
{ Extract of Obid: rational-approx-property
  normalizes to:
  
  λx,n,n. <λv.Ax, Ax, Ax>
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (|x  -  (x  within  1/n)|  \mleq{}  (r1/r(n)))


By

---

Latex:
Extract  of  Obid:  rational-approx-property
normalizes  to:

\mlambda{}x,n,n.  <\mlambda{}v.Ax,  Ax,  Ax>
finishing  with  Auto

---

Home Index