---

Step * of Lemma r-archimedean

∀x:ℝ. ∃n:ℕ. ((r(-n) ≤ x) ∧ (x ≤ r(n)))
BY
{ (InstLemma `canonical-bound-property` [] THEN ParallelLast THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `canonical-bound-property`  []  THEN  ParallelLast  THEN  Auto)

---

Home Index