---

Step * 1 1 1 1 1 1 1 of Lemma continuous-limit


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 ∈ ℝ
14. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
15. (r1/r(2 * n)) ≤ (r1/r1)
⊢ (v ∈ I) ⇒ (((z - (r1/r(2 * n))) ≤ v) ∧ (v ≤ (z + (r1/r(2 * n))))) ⇒ (v ∈ i-approx(I;2 * n))
BY
{ ((Assert (r1/r1) = r1 BY Auto) THEN (RWO "-1" (-2) THENA Auto) THEN Thin (-1)) }

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


By

---

Latex:
((Assert  (r1/r1)  =  r1  BY  Auto)  THEN  (RWO  "-1"  (-2)  THENA  Auto)  THEN  Thin  (-1))

---

Home Index