---

Step * 1 of Lemma fun-converges-to-rminus


1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. g : I ⟶ℝ
4. m : {m:ℕ+| icompact(i-approx(I;m))} 
5. k : ℕ+
6. N : ℕ+
7. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . ∀n:{N...}.  (|f[n;x] - g[x]| ≤ (r1/r(k)))
8. i-approx(I;m) ⊆ I 
9. x : {x:ℝ| x ∈ i-approx(I;m)} 
10. ∀n:{N...}. (|f[n;x] - g[x]| ≤ (r1/r(k)))
11. n : {N...}
12. |f[n;x] - g[x]| ≤ (r1/r(k))
⊢ |-(f[n;x]) - -(g[x])| ≤ (r1/r(k))
BY
{ (Assert (-(f[n;x]) - -(g[x])) = -(f[n;x] - g[x]) BY
         (nRNorm 0 THEN Auto)) }

1
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. g : I ⟶ℝ
4. m : {m:ℕ+| icompact(i-approx(I;m))} 
5. k : ℕ+
6. N : ℕ+
7. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . ∀n:{N...}.  (|f[n;x] - g[x]| ≤ (r1/r(k)))
8. i-approx(I;m) ⊆ I 
9. x : {x:ℝ| x ∈ i-approx(I;m)} 
10. ∀n:{N...}. (|f[n;x] - g[x]| ≤ (r1/r(k)))
11. n : {N...}
12. |f[n;x] - g[x]| ≤ (r1/r(k))
13. (-(f[n;x]) - -(g[x])) = -(f[n;x] - g[x])
⊢ |-(f[n;x]) - -(g[x])| ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  \mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}
3.  g  :  I  {}\mrightarrow{}\mBbbR{}
4.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\} 
5.  k  :  \mBbbN{}\msupplus{}
6.  N  :  \mBbbN{}\msupplus{}
7.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;m)\}  .  \mforall{}n:\{N...\}.    (|f[n;x]  -  g[x]|  \mleq{}  (r1/r(k)))
8.  i-approx(I;m)  \msubseteq{}  I 
9.  x  :  \{x:\mBbbR{}|  x  \mmember{}  i-approx(I;m)\} 
10.  \mforall{}n:\{N...\}.  (|f[n;x]  -  g[x]|  \mleq{}  (r1/r(k)))
11.  n  :  \{N...\}
12.  |f[n;x]  -  g[x]|  \mleq{}  (r1/r(k))
\mvdash{}  |-(f[n;x])  -  -(g[x])|  \mleq{}  (r1/r(k))


By

---

Latex:
(Assert  (-(f[n;x])  -  -(g[x]))  =  -(f[n;x]  -  g[x])  BY
              (nRNorm  0  THEN  Auto))

---

Home Index