---

Step * of Lemma converges-absolutely-converges

∀x:ℕ ⟶ ℝ. (converges-absolutely(n.x[n]) ⇒ Σn.x[n]↓)
BY
{ (Unfold `converges-absolutely` 0
   THEN Auto
   THEN ((InstLemma `comparison-test` [⌜λ2n.|x[n]|⌝])⋅ THENA Auto)
   THEN (BHyp (-1))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  (converges-absolutely(n.x[n])  {}\mRightarrow{}  \mSigma{}n.x[n]\mdownarrow{})


By

---

Latex:
(Unfold  `converges-absolutely`  0
  THEN  Auto
  THEN  ((InstLemma  `comparison-test`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.|x[n]|\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (BHyp  (-1))
  THEN  Auto)

---

Home Index