---

Step * of Lemma fun-converges-to-rminus

∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ. ∀g:I ⟶ℝ.  (lim n→∞.f[n;x] = λy.g[y] for x ∈ I ⇒ lim n→∞.-(f[n;x]) = λy.-(g[y]) for x ∈ I)
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (D -3 With ⌜m⌝  THENA Auto)
   THEN (D -1 With ⌜k⌝  THENA Auto)
   THEN (Assert i-approx(I;m) ⊆ I  BY
               Auto)
   THEN RepeatFor 2 (ParallelOp -2)
   THEN ParallelLast) }

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))
⊢ |-(f[n;x]) - -(g[x])| ≤ (r1/r(k))

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.  \mforall{}g:I  {}\mrightarrow{}\mBbbR{}.
    (lim  n\mrightarrow{}\minfty{}.f[n;x]  =  \mlambda{}y.g[y]  for  x  \mmember{}  I  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.-(f[n;x])  =  \mlambda{}y.-(g[y])  for  x  \mmember{}  I)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (D  -3  With  \mkleeneopen{}m\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  (Assert  i-approx(I;m)  \msubseteq{}  I    BY
                          Auto)
  THEN  RepeatFor  2  (ParallelOp  -2)
  THEN  ParallelLast)

---

Home Index