---

Step * of Lemma unique-limit

∀[x:ℕ ⟶ ℝ]. ∀[y1,y2:ℝ].  (y1 = y2) supposing (lim n→∞.x[n] = y2 and lim n→∞.x[n] = y1)
BY
{ (Auto
   THEN ∀h:hyp. Unfold `converges-to` h 
   THEN BLemma `infinitesmal-difference`
   THEN Auto
   THEN RepeatFor 2 ((InstHyp [⌜2 * k⌝] (-3)⋅ THENA Auto))
   THEN D -2
   THEN D -1
   THEN (Assert |x[imax(N;N1)] - y2| ≤ (r1/r(2 * k)) BY
               (Unhide THEN Auto))
   THEN (Assert |x[imax(N;N1)] - y1| ≤ (r1/r(2 * k)) BY
               (Unhide THEN Auto))) }

1
1. x : ℕ ⟶ ℝ
2. y1 : ℝ
3. y2 : ℝ
4. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - y1| ≤ (r1/r(k)))))})
5. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - y2| ≤ (r1/r(k)))))})
6. k : ℕ+
7. N : ℕ
8. [%7] : ∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - y1| ≤ (r1/r(2 * k))))
9. N1 : ℕ
10. [%9] : ∀n:ℕ. ((N1 ≤ n) ⇒ (|x[n] - y2| ≤ (r1/r(2 * k))))
11. |x[imax(N;N1)] - y2| ≤ (r1/r(2 * k))
12. |x[imax(N;N1)] - y1| ≤ (r1/r(2 * k))
⊢ |y1 - y2| ≤ (r1/r(k))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  \mforall{}h:hyp.  Unfold  `converges-to`  h 
  THEN  BLemma  `infinitesmal-difference`
  THEN  Auto
  THEN  RepeatFor  2  ((InstHyp  [\mkleeneopen{}2  *  k\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))
  THEN  D  -2
  THEN  D  -1
  THEN  (Assert  |x[imax(N;N1)]  -  y2|  \mleq{}  (r1/r(2  *  k))  BY
                          (Unhide  THEN  Auto))
  THEN  (Assert  |x[imax(N;N1)]  -  y1|  \mleq{}  (r1/r(2  *  k))  BY
                          (Unhide  THEN  Auto)))

---

Home Index