---

Step * of Lemma accelerate-rational-approx

∀[k:ℕ+]. ∀[x:ℝ]. ∀[a:ℕ+ ⟶ ℤ].  ((∀n:ℕ+. (|x - (r(a n)/r(2 * n))| ≤ (r(k)/r(n)))) ⇒ (accelerate(k;a) ∈ {y:ℝ| y = x} ))
BY
{ (InstLemma `rational-approx-implies-req` []
   THEN RepeatFor 4 (ParallelLast)
   THEN Auto
   THEN D -1
   THEN MemTypeCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbR{}].  \mforall{}[a:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].
    ((\mforall{}n:\mBbbN{}\msupplus{}.  (|x  -  (r(a  n)/r(2  *  n))|  \mleq{}  (r(k)/r(n))))  {}\mRightarrow{}  (accelerate(k;a)  \mmember{}  \{y:\mBbbR{}|  y  =  x\}  ))


By

---

Latex:
(InstLemma  `rational-approx-implies-req`  []
  THEN  RepeatFor  4  (ParallelLast)
  THEN  Auto
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index