---

Step * 1 1 1 of Lemma functions-equal-on-dense


1. I : Interval
2. X : {a:ℝ| a ∈ I}  ⟶ ℙ
3. dense-in-interval(I;X)
4. u : {a:ℝ| a ∈ I} 
5. v : {a:ℝ| a ∈ I} 
6. u ≠ v
7. f : I ⟶ℝ
8. g : I ⟶ℝ
9. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f(x) = f(y)))
10. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g(x) = g(y)))
11. ∀x:{x:ℝ| x ∈ I} . ((X x) ⇒ (f(x) = g(x)))
12. a : {x:ℝ| x ∈ I} 
13. x : ℕ ⟶ {a:ℝ| a ∈ I} 
14. ∀n:ℕ. (X (x n))
15. lim n→∞.x n = a
⊢ lim n→∞.f (x n) = f a
BY
{ (((InstLemma `function-limit` [⌜I⌝;⌜f⌝;⌜a⌝;⌜x⌝]⋅ THENM (RepUR ``r-ap so_apply`` -1 THEN Trivial)) THENA Auto)
   THEN GenConclTerm ⌜x[n]⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  X  :  \{a:\mBbbR{}|  a  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}
3.  dense-in-interval(I;X)
4.  u  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
5.  v  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
6.  u  \mneq{}  v
7.  f  :  I  {}\mrightarrow{}\mBbbR{}
8.  g  :  I  {}\mrightarrow{}\mBbbR{}
9.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y)))
10.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y)))
11.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  ((X  x)  {}\mRightarrow{}  (f(x)  =  g(x)))
12.  a  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
13.  x  :  \mBbbN{}  {}\mrightarrow{}  \{a:\mBbbR{}|  a  \mmember{}  I\} 
14.  \mforall{}n:\mBbbN{}.  (X  (x  n))
15.  lim  n\mrightarrow{}\minfty{}.x  n  =  a
\mvdash{}  lim  n\mrightarrow{}\minfty{}.f  (x  n)  =  f  a


By

---

Latex:
(((InstLemma  `function-limit`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENM  (RepUR  ``r-ap  so\_apply``  -1  THEN  Trivial))
    THENA  Auto
    )
  THEN  GenConclTerm  \mkleeneopen{}x[n]\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index