---

Step * of Lemma bdd-diff-regular-int-seq

∀[k,b:ℕ]. ∀[f:{f:ℕ+ ⟶ ℤ| k-regular-seq(f)} ]. ∀[g:ℕ+ ⟶ ℤ].
  k + b-regular-seq(g) supposing ∀n:ℕ+. (|(f n) - g n| ≤ (2 * b))
BY
{ (Auto THEN D 0 THEN Auto THEN DVar `f' THEN Unhide THEN Auto) }

1
1. k : ℕ
2. b : ℕ
3. f : ℕ+ ⟶ ℤ
4. k-regular-seq(f)
5. g : ℕ+ ⟶ ℤ
6. ∀n:ℕ+. (|(f n) - g n| ≤ (2 * b))
7. n : ℕ+@i
8. m : ℕ+@i
⊢ |(m * (g n)) - n * (g m)| ≤ ((2 * (k + b)) * (n + m))

---

Latex:

---

Latex:
\mforall{}[k,b:\mBbbN{}].  \mforall{}[f:\{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  k-regular-seq(f)\}  ].  \mforall{}[g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].
    k  +  b-regular-seq(g)  supposing  \mforall{}n:\mBbbN{}\msupplus{}.  (|(f  n)  -  g  n|  \mleq{}  (2  *  b))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  DVar  `f'  THEN  Unhide  THEN  Auto)

---

Home Index