---

Step * of Lemma ddr_wf

∀x:ℝ. ∀n:ℕ+.  (ddr(x;n) ∈ {y:ℝ| |x - y| ≤ (r1/r(5 * 10^n - 1))} )
BY
{ (Auto THEN (InstLemma `rational-approx-property` [⌜x⌝;⌜5 * 10^n - 1⌝]⋅ THENA Auto)) }

1
1. x : ℝ
2. n : ℕ+
3. |x - (x within 1/5 * 10^n - 1)| ≤ (r1/r(5 * 10^n - 1))
⊢ ddr(x;n) ∈ {y:ℝ| |x - y| ≤ (r1/r(5 * 10^n - 1))} 

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (ddr(x;n)  \mmember{}  \{y:\mBbbR{}|  |x  -  y|  \mleq{}  (r1/r(5  *  10\^{}n  -  1))\}  )


By

---

Latex:
(Auto  THEN  (InstLemma  `rational-approx-property`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}5  *  10\^{}n  -  1\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index