Step * 1 of Lemma continuous-series-sum


1. Interval@i
2. : ℕ ⟶ I ⟶ℝ@i
3. I ⟶ℝ@i
4. c1 lim n→∞{f[i;x] 0≤i≤n} = λy.g for x ∈ I@i
5. ∀n:ℕf[n;x] continuous for x ∈ I@i
⊢ continuous for y ∈ I
BY
(FLemma `fun-converges-to-continuous` [4] THEN Auto) }

1
1. Interval@i
2. : ℕ ⟶ I ⟶ℝ@i
3. I ⟶ℝ@i
4. c1 lim n→∞{f[i;x] 0≤i≤n} = λy.g for x ∈ I@i
5. ∀n:ℕf[n;x] continuous for x ∈ I@i
6. : ℕ@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