---

Step * 3 of Lemma bdd-diff-equiv


1. Sym(ℕ+ ⟶ ℤ;f,g.bdd-diff(f;g))
2. a : ℕ+ ⟶ ℤ
3. b : ℕ+ ⟶ ℤ
4. c : ℕ+ ⟶ ℤ
5. bdd-diff(a;b)
6. bdd-diff(b;c)
⊢ bdd-diff(a;c)
BY
{ (All (Unfold `bdd-diff`)
   THEN ExRepD
   THEN With ⌜B1 + B⌝ (D 0)⋅
   THEN EAuto 1
   THEN (Assert |(a n) - c n| ≤ (|(a n) - b n| + |(b n) - c n|) BY
               (RWO "int-triangle-inequality<" 0 THEN Auto))
   THEN RWO "-1" 0
   THEN Auto) }

1
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)

---

Latex:

---

Latex:

1.  Sym(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{};f,g.bdd-diff(f;g))
2.  a  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  b  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  c  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
5.  bdd-diff(a;b)
6.  bdd-diff(b;c)
\mvdash{}  bdd-diff(a;c)


By

---

Latex:
(All  (Unfold  `bdd-diff`)
  THEN  ExRepD
  THEN  With  \mkleeneopen{}B1  +  B\mkleeneclose{}  (D  0)\mcdot{}
  THEN  EAuto  1
  THEN  (Assert  |(a  n)  -  c  n|  \mleq{}  (|(a  n)  -  b  n|  +  |(b  n)  -  c  n|)  BY
                          (RWO  "int-triangle-inequality<"  0  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index