---

Step * of Lemma r-archimedean-rabs-ext

∀x:ℝ. ∃n:ℕ. (|x| ≤ r(n))
BY
{ Extract of Obid: r-archimedean-rabs
  normalizes to:
  
  λx.<canonical-bound(x), λn.<λv.Ax, Ax, Ax>>
  
  not unfolding  canonical-bound
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mexists{}n:\mBbbN{}.  (|x|  \mleq{}  r(n))


By

---

Latex:
Extract  of  Obid:  r-archimedean-rabs
normalizes  to:

\mlambda{}x.<canonical-bound(x),  \mlambda{}n.<\mlambda{}v.Ax,  Ax,  Ax>>

not  unfolding    canonical-bound
finishing  with  Auto

---

Home Index