---

Step * of Lemma continuous-series-sum

∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ. ∀cnv:Σn.f[n;x]↓ for x ∈ I.
  ((∀n:ℕ. f[n;x] continuous for x ∈ I) ⇒ Σn.f[n](y) continuous for y ∈ I)
BY
{ (Auto THEN D 3 THEN RepUR ``fun-series-sum`` 0) }

1
1. I : Interval@i
2. f : ℕ ⟶ I ⟶ℝ@i
3. g : I ⟶ℝ@i
4. c1 : lim n→∞.Σ{f[i;x] | 0≤i≤n} = λy.g y for x ∈ I@i
5. ∀n:ℕ. f[n;x] continuous for x ∈ I@i
⊢ g y continuous for y ∈ I

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.  \mforall{}cnv:\mSigma{}n.f[n;x]\mdownarrow{}  for  x  \mmember{}  I.
    ((\mforall{}n:\mBbbN{}.  f[n;x]  continuous  for  x  \mmember{}  I)  {}\mRightarrow{}  \mSigma{}n.f[n](y)  continuous  for  y  \mmember{}  I)


By

---

Latex:
(Auto  THEN  D  3  THEN  RepUR  ``fun-series-sum``  0)

---

Home Index