---

Step * 1 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. n : ℕ+
8. y ∈ i-approx(I;n)
⊢ ∃N:{ℕ| (∀m:ℕ. ((N ≤ m) ⇒ (x[m] ∈ i-approx(I;2 * n))))}
BY
{ ((With ⌜2 * n⌝ (D 4)⋅ THENA Auto)
   THEN RepeatFor 3 (ParallelLast)
   THEN (RWO "rabs-difference-bound-rleq" (-1) THENA Auto)
   THEN MoveToConcl (-1)
   THEN (Assert x[m] ∈ I BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜x[m]⌝⋅ THENA Auto)
   THEN RenameVar `z' 2) }

1
1. I : Interval
2. z : ℝ
3. x : ℕ ⟶ ℝ
4. z ∈ I
5. ∀n:ℕ. (x[n] ∈ I)
6. n : ℕ+
7. z ∈ i-approx(I;n)
8. N : ℕ
9. ∀n@0:ℕ. ((N ≤ n@0) ⇒ (|x[n@0] - z| ≤ (r1/r(2 * n))))
10. m : ℕ
11. N ≤ m
12. v : ℝ
13. x[m] = v ∈ ℝ
⊢ (v ∈ I) ⇒ (((z - (r1/r(2 * n))) ≤ v) ∧ (v ≤ (z + (r1/r(2 * n))))) ⇒ (v ∈ 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.  n  :  \mBbbN{}\msupplus{}
8.  y  \mmember{}  i-approx(I;n)
\mvdash{}  \mexists{}N:\{\mBbbN{}|  (\mforall{}m:\mBbbN{}.  ((N  \mleq{}  m)  {}\mRightarrow{}  (x[m]  \mmember{}  i-approx(I;2  *  n))))\}


By

---

Latex:
((With  \mkleeneopen{}2  *  n\mkleeneclose{}  (D  4)\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  (RWO  "rabs-difference-bound-rleq"  (-1)  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (Assert  x[m]  \mmember{}  I  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}x[m]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RenameVar  `z'  2)

---

Home Index