---

Step * of Lemma trivial-bdd-diff

∀[f,g:ℕ+ ⟶ ℤ].  bdd-diff(f;g) supposing ∀n:ℕ+. ((f n) = (g n) ∈ ℤ)
BY
{ (Auto THEN With ⌜0⌝ (D 0)⋅ THEN Auto THEN RWO "-2" 0 THEN Auto) }

1
1. f : ℕ+ ⟶ ℤ
2. g : ℕ+ ⟶ ℤ
3. ∀n:ℕ+. ((f n) = (g n) ∈ ℤ)
4. n : ℕ+@i
⊢ |(g n) - g n| ≤ 0

---

Latex:

---

Latex:
\mforall{}[f,g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].    bdd-diff(f;g)  supposing  \mforall{}n:\mBbbN{}\msupplus{}.  ((f  n)  =  (g  n))


By

---

Latex:
(Auto  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index