---

Step * of Lemma bdd-diff-iff-eventual

∀f,g:ℕ+ ⟶ ℤ.  (∃m:ℕ+. ∃B:ℕ. ∀n:{m...}. (|(f n) - g n| ≤ B) ⇐⇒ bdd-diff(f;g))
BY
{ Auto }

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index