---

Step * 1 of Lemma converges-iff-cauchy


1. x : ℕ ⟶ ℝ
2. x[n]↓ as n→∞
⊢ cauchy(n.x[n])
BY
{ TACTIC:((D (-1))
          THEN Unfold `converges-to` -1
          THEN D 0
          THEN Auto
          THEN ((InstHyp [⌜2 * k⌝] (-2))⋅ THENA Auto')
          THEN D -1
          THEN (Assert ∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - y| ≤ (r1/r(2 * k)))) BY
                      (Unhide THEN Try (Trivial) THEN Auto))
          THEN Thin (-2)) }

1
1. x : ℕ ⟶ ℝ
2. y : ℝ
3. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - y| ≤ (r1/r(k)))))])
4. k : ℕ+
5. N : ℕ
6. ∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - y| ≤ (r1/r(2 * k))))
⊢ ∃N:ℕ [(∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ m) ⇒ (|x[n] - x[m]| ≤ (r1/r(k)))))]

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  x[n]\mdownarrow{}  as  n\mrightarrow{}\minfty{}
\mvdash{}  cauchy(n.x[n])


By

---

Latex:
TACTIC:((D  (-1))
                THEN  Unfold  `converges-to`  -1
                THEN  D  0
                THEN  Auto
                THEN  ((InstHyp  [\mkleeneopen{}2  *  k\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto')
                THEN  D  -1
                THEN  (Assert  \mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|x[n]  -  y|  \mleq{}  (r1/r(2  *  k))))  BY
                                        (Unhide  THEN  Try  (Trivial)  THEN  Auto))
                THEN  Thin  (-2))

---

Home Index