---

Step * of Lemma total-function-limit

∀f:ℝ ⟶ ℝ. ∀y:ℝ. ∀x:ℕ ⟶ ℝ.  ((∀x,y:ℝ.  ((x = y) ⇒ (f[x] = f[y]))) ⇒ lim n→∞.x[n] = y ⇒ lim n→∞.f[x[n]] = f[y])
BY
{ ((InstLemma `continuous-limit` [⌜(-∞, ∞)⌝]⋅ THENA Auto) THEN RepeatFor 4 ((ParallelLast' THENA Auto))) }

1
.....antecedent..... 
1. f : ℝ ⟶ ℝ
2. y : ℝ
3. x : ℕ ⟶ ℝ
4. ∀x,y:ℝ.  ((x = y) ⇒ (f[x] = f[y]))
⊢ f(x) continuous for x ∈ (-∞, ∞)

2
1. f : ℝ ⟶ ℝ
2. y : ℝ
3. x : ℕ ⟶ ℝ
4. ∀x,y:ℝ.  ((x = y) ⇒ (f[x] = f[y]))
5. lim n→∞.x[n] = y ⇒ (y ∈ (-∞, ∞)) ⇒ (∀n:ℕ. (x[n] ∈ (-∞, ∞))) ⇒ lim n→∞.f(x[n]) = f(y)
⊢ lim n→∞.x[n] = y ⇒ lim n→∞.f[x[n]] = f[y]

---

Latex:

---

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


By

---

Latex:
((InstLemma  `continuous-limit`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  )

---

Home Index