---

Step * of Lemma continuous-sum

No Annotations
∀I:Interval. ∀n,m:ℤ. ∀f:{n..m + 1-} ⟶ I ⟶ℝ.
  ((∀i:{n..m + 1-}. f[i;x] continuous for x ∈ I) ⇒ Σ{f[i;x] | n≤i≤m} continuous for x ∈ I)
BY
{ (Auto THEN Assert ⌜∀d:ℕ. (((n + d) ≤ m) ⇒ Σ{f[i;x] | n≤i≤n + d} continuous for x ∈ I)⌝⋅) }

1
.....assertion..... 
1. I : Interval
2. n : ℤ
3. m : ℤ
4. f : {n..m + 1-} ⟶ I ⟶ℝ
5. ∀i:{n..m + 1-}. f[i;x] continuous for x ∈ I
⊢ ∀d:ℕ. (((n + d) ≤ m) ⇒ Σ{f[i;x] | n≤i≤n + d} continuous for x ∈ I)

2
1. I : Interval
2. n : ℤ
3. m : ℤ
4. f : {n..m + 1-} ⟶ I ⟶ℝ
5. ∀i:{n..m + 1-}. f[i;x] continuous for x ∈ I
6. ∀d:ℕ. (((n + d) ≤ m) ⇒ Σ{f[i;x] | n≤i≤n + d} continuous for x ∈ I)
⊢ Σ{f[i;x] | n≤i≤m} continuous for x ∈ I

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval.  \mforall{}n,m:\mBbbZ{}.  \mforall{}f:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}i:\{n..m  +  1\msupminus{}\}.  f[i;x]  continuous  for  x  \mmember{}  I)  {}\mRightarrow{}  \mSigma{}\{f[i;x]  |  n\mleq{}i\mleq{}m\}  continuous  for  x  \mmember{}  I)


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  (((n  +  d)  \mleq{}  m)  {}\mRightarrow{}  \mSigma{}\{f[i;x]  |  n\mleq{}i\mleq{}n  +  d\}  continuous  for  x  \mmember{}  I)\mkleeneclose{}\mcdot{})

---

Home Index