---

Step * of Lemma rational-approx-property1

∀x:ℝ. ∀n:ℕ+.  (x ≤ ((x within 1/n) + (r1/r(n))))
BY
{ (InstLemma `rational-approx-property-ext` []⋅ THEN RepeatFor 2 (ParallelLast')) }

1
1. x : ℝ@i
2. n : ℕ+@i
3. |x - (x within 1/n)| ≤ (r1/r(n))
⊢ x ≤ ((x within 1/n) + (r1/r(n)))

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rational-approx-property-ext`  []\mcdot{}  THEN  RepeatFor  2  (ParallelLast'))

---

Home Index