---

Step * of Lemma functions-equal-on-dense

No Annotations
∀I:Interval
  ∀[X:{a:ℝ| a ∈ I}  ⟶ ℙ]
    (dense-in-interval(I;X)
    ⇒ (∃u,v:{a:ℝ| a ∈ I} . u ≠ v)
    ⇒ (∀f,g:I ⟶ℝ.
          ((∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f(x) = f(y))))
          ⇒ (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g(x) = g(y))))
          ⇒ (∀x:{x:ℝ| x ∈ I} . ((X x) ⇒ (f(x) = g(x))))
          ⇒ (∀a:{x:ℝ| x ∈ I} . (f(a) = g(a))))))
BY
{ (Auto THEN (InstLemma `dense-in-interval-implies` [⌜I⌝;⌜X⌝;⌜a⌝]⋅ THENA Auto) THEN ExRepD) }

1
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval
    \mforall{}[X:\{a:\mBbbR{}|  a  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}]
        (dense-in-interval(I;X)
        {}\mRightarrow{}  (\mexists{}u,v:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  u  \mneq{}  v)
        {}\mRightarrow{}  (\mforall{}f,g:I  {}\mrightarrow{}\mBbbR{}.
                    ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))
                    {}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y))))
                    {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  ((X  x)  {}\mRightarrow{}  (f(x)  =  g(x))))
                    {}\mRightarrow{}  (\mforall{}a:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f(a)  =  g(a))))))


By

---

Latex:
(Auto  THEN  (InstLemma  `dense-in-interval-implies`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index