---

Step * of Lemma ireal-approx-1

∀[x:ℝ]. ∀[M:ℕ+].  1-approx(x;M;x M)
BY
{ (Auto THEN Unfold `ireal-approx` 0) }

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

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[M:\mBbbN{}\msupplus{}].    1-approx(x;M;x  M)


By

---

Latex:
(Auto  THEN  Unfold  `ireal-approx`  0)

---

Home Index