---

Step * of Lemma rational-approx-property

∀x:ℝ. ∀n:ℕ+.  (|x - (x within 1/n)| ≤ (r1/r(n)))
BY
{ (Auto
   THEN (Unfold `rational-approx` 0 THEN (RWO "int-rdiv-req" 0 THENA Auto))
   THEN nRMul ⌜r(n)⌝ 0⋅
   THEN nRMul ⌜r(2)⌝ 0⋅) }

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Unfold  `rational-approx`  0  THEN  (RWO  "int-rdiv-req"  0  THENA  Auto))
  THEN  nRMul  \mkleeneopen{}r(n)\mkleeneclose{}  0\mcdot{}
  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{})

---

Home Index