---

Step * of Lemma fun-comparison-test

No Annotations
∀I:Interval. ∀f,g:ℕ ⟶ I ⟶ℝ.
  (Σn.g[n;x]↓ for x ∈ I ⇒ (∀n:ℕ. ∀x:{x:ℝ| x ∈ I} .  (|f[n;x]| ≤ g[n;x])) ⇒ Σn.f[n;x]↓ for x ∈ I)
BY
{ (Auto
   THEN All (RepUR ``fun-series-converges``)
   THEN All (RWO "fun-converges-iff-cauchy")
   THEN Auto
   THEN RepeatFor 2 (ParallelOp -2)
   THEN Thin 4) }

1
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. g : ℕ ⟶ I ⟶ℝ
4. ∀n:ℕ. ∀x:{x:ℝ| x ∈ I} .  (|f[n;x]| ≤ g[n;x])
5. a : {a:ℕ+| icompact(i-approx(I;a))} 
6. ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . ∀n,m:{N...}.  (|Σ{g[i;x] | 0≤i≤n} - Σ{g[i;x] | 0≤i≤m}| ≤ (r1/r(k)))
⊢ ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . ∀n,m:{N...}.  (|Σ{f[i;x] | 0≤i≤n} - Σ{f[i;x] | 0≤i≤m}| ≤ (r1/r(k)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.
    (\mSigma{}n.g[n;x]\mdownarrow{}  for  x  \mmember{}  I  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (|f[n;x]|  \mleq{}  g[n;x]))  {}\mRightarrow{}  \mSigma{}n.f[n;x]\mdownarrow{}  for  x  \mmember{}  I)


By

---

Latex:
(Auto
  THEN  All  (RepUR  ``fun-series-converges``)
  THEN  All  (RWO  "fun-converges-iff-cauchy")
  THEN  Auto
  THEN  RepeatFor  2  (ParallelOp  -2)
  THEN  Thin  4)

---

Home Index