---

Step * of Lemma fun-series-converges-absolutely-converges

∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ.  (Σn.f[n;x]↓ absolutely for x ∈ I ⇒ Σn.f[n;x]↓ for x ∈ I)
BY
{ ((InstLemma `fun-comparison-test` []
    THEN RepeatFor 2 (ParallelLast')
    THEN Unfold `fun-series-converges-absolutely` 0
    THEN (With ⌜λn,x. |f[n;x]|⌝ (D (-1))⋅ THENA Auto))
   THEN All (RepUR ``so_apply``)
   THEN ParallelLast
   THEN BHyp -1 
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((InstLemma  `fun-comparison-test`  []
    THEN  RepeatFor  2  (ParallelLast')
    THEN  Unfold  `fun-series-converges-absolutely`  0
    THEN  (With  \mkleeneopen{}\mlambda{}n,x.  |f[n;x]|\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto))
  THEN  All  (RepUR  ``so\_apply``)
  THEN  ParallelLast
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index