---

Step * of Lemma eventually-equal-implies-bdd-diff

∀f,g:ℕ+ ⟶ ℤ.  ((∃m:ℕ+. ∀n:{m...}. ((f n) = (g n) ∈ ℤ)) ⇒ bdd-diff(f;g))
BY
{ (Auto THEN (BLemma `bdd-diff-iff-eventual` THENA Auto) THEN ParallelLast) }

1
1. f : ℕ+ ⟶ ℤ
2. g : ℕ+ ⟶ ℤ
3. m : ℕ+
4. ∀n:{m...}. ((f n) = (g n) ∈ ℤ)
⊢ ∃B:ℕ. ∀n:{m...}. (|(f n) - g n| ≤ B)

---

Latex:

---

Latex:
\mforall{}f,g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.    ((\mexists{}m:\mBbbN{}\msupplus{}.  \mforall{}n:\{m...\}.  ((f  n)  =  (g  n)))  {}\mRightarrow{}  bdd-diff(f;g))


By

---

Latex:
(Auto  THEN  (BLemma  `bdd-diff-iff-eventual`  THENA  Auto)  THEN  ParallelLast)

---

Home Index