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