---

Step * of Lemma integer-approx_wf

∀[x:ℝ]. ∀[k:ℕ+].  (integer-approx(x;k) ∈ {n:ℤ| |x - r(n)| ≤ (r1 + (r1/r(k)))} )
BY
{ (ProveWfLemma
   THEN MemTypeCD
   THEN Auto
   THEN (InstLemma `rational-approx-property` [⌜x⌝;⌜k⌝]⋅ THENA Auto)
   THEN UseTriangleInequality [⌜(x within 1/k)⌝]⋅) }

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

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[k:\mBbbN{}\msupplus{}].    (integer-approx(x;k)  \mmember{}  \{n:\mBbbZ{}|  |x  -  r(n)|  \mleq{}  (r1  +  (r1/r(k)))\}  )


By

---

Latex:
(ProveWfLemma
  THEN  MemTypeCD
  THEN  Auto
  THEN  (InstLemma  `rational-approx-property`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  UseTriangleInequality  [\mkleeneopen{}(x  within  1/k)\mkleeneclose{}]\mcdot{})

---

Home Index