---

Step * 1 1 of Lemma continuous-limit


1. I : Interval
2. y : ℝ
3. x : ℕ ⟶ ℝ
4. lim n→∞.x[n] = y
5. y ∈ I
6. ∀n:ℕ. (x[n] ∈ I)
7. k : ℕ+
8. n : ℕ+
9. y ∈ i-approx(I;n)
10. y ∈ i-approx(I;2 * n)
11. icompact(i-approx(I;2 * n))
12. d : ℝ
13. r0 < d
⊢ ∃N:{ℕ| (∀m:ℕ. ((N ≤ m) ⇒ ((x[m] ∈ i-approx(I;2 * n)) ∧ (|x[m] - y| ≤ d))))}
BY
{ (Assert ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - y| ≤ d)))} BY
         ((InstLemma `small-reciprocal-real` [⌜d⌝]⋅ THENA Auto)
          THEN D -1
          THEN With ⌜k1⌝ (D 4) ⋅
          THEN Auto
          THEN RepeatFor 3 (ParallelLast)
          THEN Auto)) }

1
1. I : Interval
2. y : ℝ
3. x : ℕ ⟶ ℝ
4. lim n→∞.x[n] = y
5. y ∈ I
6. ∀n:ℕ. (x[n] ∈ I)
7. k : ℕ+
8. n : ℕ+
9. y ∈ i-approx(I;n)
10. y ∈ i-approx(I;2 * n)
11. icompact(i-approx(I;2 * n))
12. d : ℝ
13. r0 < d
14. ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - y| ≤ d)))}
⊢ ∃N:{ℕ| (∀m:ℕ. ((N ≤ m) ⇒ ((x[m] ∈ i-approx(I;2 * n)) ∧ (|x[m] - y| ≤ d))))}

---

Latex:

---

Latex:

1.  I  :  Interval
2.  y  :  \mBbbR{}
3.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
4.  lim  n\mrightarrow{}\minfty{}.x[n]  =  y
5.  y  \mmember{}  I
6.  \mforall{}n:\mBbbN{}.  (x[n]  \mmember{}  I)
7.  k  :  \mBbbN{}\msupplus{}
8.  n  :  \mBbbN{}\msupplus{}
9.  y  \mmember{}  i-approx(I;n)
10.  y  \mmember{}  i-approx(I;2  *  n)
11.  icompact(i-approx(I;2  *  n))
12.  d  :  \mBbbR{}
13.  r0  <  d
\mvdash{}  \mexists{}N:\{\mBbbN{}|  (\mforall{}m:\mBbbN{}.  ((N  \mleq{}  m)  {}\mRightarrow{}  ((x[m]  \mmember{}  i-approx(I;2  *  n))  \mwedge{}  (|x[m]  -  y|  \mleq{}  d))))\}


By

---

Latex:
(Assert  \mexists{}N:\{\mBbbN{}|  (\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|x[n]  -  y|  \mleq{}  d)))\}  BY
              ((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  With  \mkleeneopen{}k1\mkleeneclose{}  (D  4)  \mcdot{}
                THEN  Auto
                THEN  RepeatFor  3  (ParallelLast)
                THEN  Auto))

---

Home Index