---

Step * of Lemma mconverges-to_functionality

∀[X:Type]. ∀d:metric(X). ∀x1,x2:ℕ ⟶ X.  ∀[y:X]. {lim n→∞.x1[n] = y ⇒ lim n→∞.x2[n] = y} supposing ∀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)
   THEN RepeatFor 3 (ParallelLast)
   THEN ((InstHyp [⌜n⌝] 6)⋅ THENA Auto)
   THEN Assert ⌜mdist(d;x1[n];y) = mdist(d;x2[n];y)⌝⋅
   THEN Auto
   THEN BLemma `mdist_functionality`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}x1,x2:\mBbbN{}  {}\mrightarrow{}  X.
        \mforall{}[y:X].  \{lim  n\mrightarrow{}\minfty{}.x1[n]  =  y  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x2[n]  =  y\}  supposing  \mforall{}n:\mBbbN{}.  x1[n]  \mequiv{}  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)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  ((InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  6)\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}mdist(d;x1[n];y)  =  mdist(d;x2[n];y)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  BLemma  `mdist\_functionality`
  THEN  Auto)

---

Home Index