---

Step * of Lemma limit-shift-iff

∀m:ℕ. ∀X:ℕ ⟶ ℝ. ∀a:ℝ.  (lim n→∞.X[n] = a ⇐⇒ lim n→∞.X[n + m] = a)
BY
{ (InstLemma `limit-shift` [] THEN RepeatFor 3 (ParallelLast') THEN Auto) }

1
1. m : ℕ
2. X : ℕ ⟶ ℝ
3. a : ℝ
4. lim n→∞.X[n] = a ⇒ lim n→∞.X[n + m] = a
5. lim n→∞.X[n + m] = a
⊢ lim n→∞.X[n] = a

---

Latex:

---

Latex:
\mforall{}m:\mBbbN{}.  \mforall{}X:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}a:\mBbbR{}.    (lim  n\mrightarrow{}\minfty{}.X[n]  =  a  \mLeftarrow{}{}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.X[n  +  m]  =  a)


By

---

Latex:
(InstLemma  `limit-shift`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  Auto)

---

Home Index