---

Step * of Lemma m-unique-limit

∀[X:Type]. ∀d:metric(X). ∀x:ℕ ⟶ X.  ∀[y1,y2:X].  (y1 ≡ y2) supposing (lim n→∞.x[n] = y1 and lim n→∞.x[n] = y2)
BY
{ (Auto THEN ∀h:hyp. Unfold `mconverges-to` h  THEN Unfold `meq` 0) }

1
1. X : Type
2. d : metric(X)
3. x : ℕ ⟶ X
4. y1 : X
5. y2 : X
6. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x[n];y2) ≤ (r1/r(k)))))])
7. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x[n];y1) ≤ (r1/r(k)))))])
⊢ (d y1 y2) = r0

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.
        \mforall{}[y1,y2:X].    (y1  \mequiv{}  y2)  supposing  (lim  n\mrightarrow{}\minfty{}.x[n]  =  y1  and  lim  n\mrightarrow{}\minfty{}.x[n]  =  y2)


By

---

Latex:
(Auto  THEN  \mforall{}h:hyp.  Unfold  `mconverges-to`  h    THEN  Unfold  `meq`  0)

---

Home Index