---

Step * 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
⊢ f(a) = g(a)
BY
{ Assert ⌜lim n→∞.f (x n) = f a ∧ lim n→∞.g (x n) = g a⌝⋅ }

1
.....assertion..... 
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 ∧ lim n→∞.g (x n) = g a

2
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
16. lim n→∞.f (x n) = f a ∧ lim n→∞.g (x n) = g a
⊢ f(a) = g(a)

---

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{}  f(a)  =  g(a)


By

---

Latex:
Assert  \mkleeneopen{}lim  n\mrightarrow{}\minfty{}.f  (x  n)  =  f  a  \mwedge{}  lim  n\mrightarrow{}\minfty{}.g  (x  n)  =  g  a\mkleeneclose{}\mcdot{}

---

Home Index