---

Step * 1 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
14. ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - y| ≤ d)))}
⊢ ∃N:{ℕ| (∀m:ℕ. ((N ≤ m) ⇒ ((x[m] ∈ i-approx(I;2 * n)) ∧ (|x[m] - y| ≤ d))))}
BY
{ ((Assert ⌜∃N:{ℕ| (∀m:ℕ. ((N ≤ m) ⇒ (x[m] ∈ i-approx(I;2 * n))))}⌝⋅
   THENM (D -2 THEN D -1 THEN With ⌜imax(N;N1)⌝ (D 0)⋅ THEN Auto THEN ∀h:hyp. (RWO "imax_lb" h⋅ THEN Auto) )
   )
   THEN ThinVar `d'
   THEN ThinVar `k'
   THEN RepeatFor 2 (Thin (-1))) }

1
1. I : Interval
2. y : ℝ
3. x : ℕ ⟶ ℝ
4. lim n→∞.x[n] = y
5. y ∈ I
6. ∀n:ℕ. (x[n] ∈ I)
7. n : ℕ+
8. y ∈ i-approx(I;n)
⊢ ∃N:{ℕ| (∀m:ℕ. ((N ≤ m) ⇒ (x[m] ∈ i-approx(I;2 * n))))}

---

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
14.  \mexists{}N:\{\mBbbN{}|  (\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|x[n]  -  y|  \mleq{}  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  \mkleeneopen{}\mexists{}N:\{\mBbbN{}|  (\mforall{}m:\mBbbN{}.  ((N  \mleq{}  m)  {}\mRightarrow{}  (x[m]  \mmember{}  i-approx(I;2  *  n))))\}\mkleeneclose{}\mcdot{}
  THENM  (D  -2
                THEN  D  -1
                THEN  With  \mkleeneopen{}imax(N;N1)\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Auto
                THEN  \mforall{}h:hyp.  (RWO  "imax\_lb"  h\mcdot{}  THEN  Auto)  )
  )
  THEN  ThinVar  `d'
  THEN  ThinVar  `k'
  THEN  RepeatFor  2  (Thin  (-1)))

---

Home Index