Step
*
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
⊢ g y continuous for y ∈ I
BY
{ (FLemma `fun-converges-to-continuous` [4] THEN Auto) }
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
6. n : ℕ@i
⊢ Σ{f[i;x] | 0≤i≤n} continuous for x ∈ I
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
\mvdash{}  g  y  continuous  for  y  \mmember{}  I
By
Latex:
(FLemma  `fun-converges-to-continuous`  [4]  THEN  Auto)
Home
Index