---

Step * of Lemma implies-regular

∀[k:ℕ+]. ∀[x:ℕ+ ⟶ ℤ].
  k-regular-seq(x) supposing ∀n,m:ℕ+.  (|(x within 1/n) - (x within 1/m)| ≤ ((r(k)/r(n)) + (r(k)/r(m))))
BY
{ (Unfold `rational-approx` 0 THEN Auto THEN UnfoldTopAb 0 THEN RepeatFor 2 (ParallelLast')) }

1
1. k : ℕ+
2. x : ℕ+ ⟶ ℤ
3. n : ℕ+
4. m : ℕ+
5. |(r(x n))/2 * n - (r(x m))/2 * m| ≤ ((r(k)/r(n)) + (r(k)/r(m)))
⊢ |(m * (x n)) - n * (x m)| ≤ ((2 * k) * (n + m))

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].
    k-regular-seq(x) 
    supposing  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(x  within  1/n)  -  (x  within  1/m)|  \mleq{}  ((r(k)/r(n))  +  (r(k)/r(m))))


By

---

Latex:
(Unfold  `rational-approx`  0  THEN  Auto  THEN  UnfoldTopAb  0  THEN  RepeatFor  2  (ParallelLast'))

---

Home Index