---

Step * 3 1 of Lemma bdd-diff-equiv


1. Sym(ℕ+ ⟶ ℤ;f,g.∃B:ℕ. ∀n:ℕ+. (|(f n) - g n| ≤ B))
2. a : ℕ+ ⟶ ℤ
3. b : ℕ+ ⟶ ℤ
4. c : ℕ+ ⟶ ℤ
5. B1 : ℕ
6. ∀n:ℕ+. (|(a n) - b n| ≤ B1)
7. B : ℕ
8. ∀n:ℕ+. (|(b n) - c n| ≤ B)
9. n : ℕ+
10. |(a n) - c n| ≤ (|(a n) - b n| + |(b n) - c n|)
⊢ (|(a n) - b n| + |(b n) - c n|) ≤ (B1 + B)
BY
{ (RWO "6 8" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Sym(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{};f,g.\mexists{}B:\mBbbN{}.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(f  n)  -  g  n|  \mleq{}  B))
2.  a  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  b  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  c  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
5.  B1  :  \mBbbN{}
6.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(a  n)  -  b  n|  \mleq{}  B1)
7.  B  :  \mBbbN{}
8.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(b  n)  -  c  n|  \mleq{}  B)
9.  n  :  \mBbbN{}\msupplus{}
10.  |(a  n)  -  c  n|  \mleq{}  (|(a  n)  -  b  n|  +  |(b  n)  -  c  n|)
\mvdash{}  (|(a  n)  -  b  n|  +  |(b  n)  -  c  n|)  \mleq{}  (B1  +  B)


By

---

Latex:
(RWO  "6  8"  0  THEN  Auto)\mcdot{}

---

Home Index