---

Step * 1 of Lemma continuous-limit


1. I : Interval
2. f : I ⟶ℝ
3. y : ℝ
4. x : ℕ ⟶ ℝ
5. ∀m:{m:ℕ+| icompact(i-approx(I;m))} . ∀n:ℕ+.
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f(x) - f(y)| ≤ (r1/r(n))))))})
6. lim n→∞.x[n] = y
7. y ∈ I
8. ∀n:ℕ. (x[n] ∈ I)
9. k : ℕ+
10. n : ℕ+
11. y ∈ i-approx(I;n)
12. y ∈ i-approx(I;2 * n)
13. icompact(i-approx(I;2 * n))
14. d : ℝ
15. [%26] : (r0 < d)
∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;2 * n)) ⇒ (y ∈ i-approx(I;2 * n)) ⇒ (|x - y| ≤ d) ⇒ (|f(x) - f(y)| ≤ (r1/r(k)))))
⊢ ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|f(x[n]) - f(y)| ≤ (r1/r(k)))))}
BY
{ ((Assert ⌜∃N:{ℕ| (∀m:ℕ. ((N ≤ m) ⇒ ((x[m] ∈ i-approx(I;2 * n)) ∧ (|x[m] - y| ≤ d))))}⌝⋅
   THENM (RepeatFor 3 (ParallelLast) THEN Auto)
   )
   THEN (Assert r0 < d BY
               (Unhide THEN Auto))
   THEN ThinVar `f') }

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
⊢ ∃N:{ℕ| (∀m:ℕ. ((N ≤ m) ⇒ ((x[m] ∈ i-approx(I;2 * n)) ∧ (|x[m] - y| ≤ d))))}

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mkleeneopen{}\mexists{}N:\{\mBbbN{}|  (\mforall{}m:\mBbbN{}.  ((N  \mleq{}  m)  {}\mRightarrow{}  ((x[m]  \mmember{}  i-approx(I;2  *  n))  \mwedge{}  (|x[m]  -  y|  \mleq{}  d))))\}\mkleeneclose{}\mcdot{}
  THENM  (RepeatFor  3  (ParallelLast)  THEN  Auto)
  )
  THEN  (Assert  r0  <  d  BY
                          (Unhide  THEN  Auto))
  THEN  ThinVar  `f')

---

Home Index