---

Step * of Lemma rless-implies-rleq

∀x,y:ℝ.  ((x < y) ⇒ (∃m:ℕ+. (x ≤ (y - (r1/r(m))))))
BY
{ (InstLemma `rless-iff-rleq` [] THEN RepeatFor 2 (ParallelLast') THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((x  <  y)  {}\mRightarrow{}  (\mexists{}m:\mBbbN{}\msupplus{}.  (x  \mleq{}  (y  -  (r1/r(m))))))


By

---

Latex:
(InstLemma  `rless-iff-rleq`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  Auto)

---

Home Index