---

Step * of Lemma function-limit

∀I:Interval. ∀f:I ⟶ℝ. ∀y:ℝ. ∀x:ℕ ⟶ ℝ.
  ((∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f(x) = f(y))))
  ⇒ lim n→∞.x[n] = y
  ⇒ (y ∈ I)
  ⇒ (∀n:ℕ. (x[n] ∈ I))
  ⇒ lim n→∞.f(x[n]) = f(y))
BY
{ (InstLemma `continuous-limit` []
   THEN RepeatFor 5 (ParallelLast')
   THEN Auto
   THEN BLemma `function-is-continuous`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}y:\mBbbR{}.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))
    {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  =  y
    {}\mRightarrow{}  (y  \mmember{}  I)
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (x[n]  \mmember{}  I))
    {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.f(x[n])  =  f(y))


By

---

Latex:
(InstLemma  `continuous-limit`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  Auto
  THEN  BLemma  `function-is-continuous`
  THEN  Auto)

---

Home Index