---

Step * of Lemma subsequence-mconverges

∀[X:Type]. ∀[d:metric(X)]. ∀[a:X].  ∀x,y:ℕ ⟶ X.  (subsequence(a,b.a ≡ b;n.x[n];n.y[n]) ⇒ x[n]↓ as n→∞ ⇒ y[n]↓ as n→∞)
BY
{ (Auto THEN RepeatFor 2 (ParallelLast) THEN FLemma `subsequence-mconverges-to` [-3;-1] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[a:X].
    \mforall{}x,y:\mBbbN{}  {}\mrightarrow{}  X.    (subsequence(a,b.a  \mequiv{}  b;n.x[n];n.y[n])  {}\mRightarrow{}  x[n]\mdownarrow{}  as  n\mrightarrow{}\minfty{}  {}\mRightarrow{}  y[n]\mdownarrow{}  as  n\mrightarrow{}\minfty{})


By

---

Latex:
(Auto  THEN  RepeatFor  2  (ParallelLast)  THEN  FLemma  `subsequence-mconverges-to`  [-3;-1]  THEN  Auto)

---

Home Index