---

Step * of Lemma fun-series-converges-tail

∀M:ℕ. ∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ.  (Σn.f[n + M;x]↓ for x ∈ I ⇒ Σn.f[n;x]↓ for x ∈ I)
BY
{ TACTIC:(Auto
          THEN ParallelLast
          THEN (RWO "fun-converges-iff-cauchy" (-1) THENA Auto)
          THEN BLemma `fun-converges-iff-cauchy`
          THEN Auto
          THEN RepeatFor 3 (ParallelLast')
          THEN ExRepD
          THEN With ⌜N + M⌝ (D 0)⋅
          THEN Auto
          THEN Try (Complete ((DSetVars THEN ∀h:hyp. (FLemma `i-member-approx` [h] THEN Auto) )))) }

1
1. M : ℕ
2. I : Interval
3. f : ℕ ⟶ I ⟶ℝ
4. a : {a:ℕ+| icompact(i-approx(I;a))} 
5. k : ℕ+
6. N : ℕ+
7. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . ∀n,m:{N...}.  (|Σ{f[i + M;x] | 0≤i≤n} - Σ{f[i + M;x] | 0≤i≤m}| ≤ (r1/r(k)))
8. x : {x:ℝ| x ∈ i-approx(I;a)} 
9. n : {N + M...}
10. m : {N + M...}
⊢ |Σ{f[i;x] | 0≤i≤n} - Σ{f[i;x] | 0≤i≤m}| ≤ (r1/r(k))

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto
                THEN  ParallelLast
                THEN  (RWO  "fun-converges-iff-cauchy"  (-1)  THENA  Auto)
                THEN  BLemma  `fun-converges-iff-cauchy`
                THEN  Auto
                THEN  RepeatFor  3  (ParallelLast')
                THEN  ExRepD
                THEN  With  \mkleeneopen{}N  +  M\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Auto
                THEN  Try  (Complete  ((DSetVars  THEN  \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THEN  Auto)  ))))

---

Home Index