---

Step * 1 1 of Lemma continuous-series-sum


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
6. n : ℕ@i
⊢ Σ{f[i;x] | 0≤i≤n} continuous for x ∈ I
BY
{ (ProveRealContinuous THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  f  :  \mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}@i
3.  g  :  I  {}\mrightarrow{}\mBbbR{}@i
4.  c1  :  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{f[i;x]  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}y.g  y  for  x  \mmember{}  I@i
5.  \mforall{}n:\mBbbN{}.  f[n;x]  continuous  for  x  \mmember{}  I@i
6.  n  :  \mBbbN{}@i
\mvdash{}  \mSigma{}\{f[i;x]  |  0\mleq{}i\mleq{}n\}  continuous  for  x  \mmember{}  I


By

---

Latex:
(ProveRealContinuous  THEN  Auto)

---

Home Index