---

Step * of Lemma rational-approx-property2

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

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

---

Latex:

---

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


By

---

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

---

Home Index