---

Step * of Lemma converges-to_functionality

∀x1,x2:ℕ ⟶ ℝ. ∀y1,y2:ℝ.  ({lim n→∞.x1[n] = y1 ⇒ lim n→∞.x2[n] = y2}) supposing ((y1 = y2) and (∀n:ℕ. (x1[n] = x2[n])))
BY
{ ((Unfold `guard` 0 THEN Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN (Assert (r1/r(k)) ∈ ℝ BY
               (Auto THEN BLemma `rneq-int` THEN Auto))
   THEN PromoteHyp (-1) (-2)) }

1
1. x1 : ℕ ⟶ ℝ@i
2. x2 : ℕ ⟶ ℝ@i
3. y1 : ℝ@i
4. y2 : ℝ@i
5. ∀n:ℕ. (x1[n] = x2[n])
6. y1 = y2
7. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x1[n] - y1| ≤ (r1/r(k)))))})@i
8. k : ℕ+@i
9. (r1/r(k)) ∈ ℝ
10. ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x1[n] - y1| ≤ (r1/r(k)))))}
⊢ ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x2[n] - y2| ≤ (r1/r(k)))))}

---

Latex:

---

Latex:
\mforall{}x1,x2:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}y1,y2:\mBbbR{}.
    (\{lim  n\mrightarrow{}\minfty{}.x1[n]  =  y1  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x2[n]  =  y2\})  supposing  ((y1  =  y2)  and  (\mforall{}n:\mBbbN{}.  (x1[n]  =  x2[n])))


By

---

Latex:
((Unfold  `guard`  0  THEN  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (Assert  (r1/r(k))  \mmember{}  \mBbbR{}  BY
                          (Auto  THEN  BLemma  `rneq-int`  THEN  Auto))
  THEN  PromoteHyp  (-1)  (-2))

---

Home Index