---

Step * of Lemma functions-equal-on-rationals

∀I:Interval
  ((∃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))))
        ⇒ (∀z:ℤ. ∀d:ℕ+.  (((r(z)/r(d)) ∈ I) ⇒ (f((r(z)/r(d))) = g((r(z)/r(d))))))
        ⇒ (∀a:{x:ℝ| x ∈ I} . (f(a) = g(a))))))
BY
{ (Auto THEN InstLemma `functions-equal-on-dense`  [⌜I⌝;⌜λr.∃z:ℤ. ∃d:ℕ+. (r = (r(z)/r(d)))⌝;⌜f⌝;⌜g⌝;⌜a⌝]⋅ THEN Auto) }

1
1. I : Interval
2. ∃u,v:{a:ℝ| a ∈ I} . u ≠ v
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f(x) = f(y)))
6. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g(x) = g(y)))
7. ∀z:ℤ. ∀d:ℕ+.  (((r(z)/r(d)) ∈ I) ⇒ (f((r(z)/r(d))) = g((r(z)/r(d)))))
8. a : {x:ℝ| x ∈ I} 
9. x : {x:ℝ| x ∈ I} 
10. (λr.∃z:ℤ. ∃d:ℕ+. (r = (r(z)/r(d)))) x
⊢ f(x) = g(x)

---

Latex:

---

Latex:
\mforall{}I:Interval
    ((\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{}z:\mBbbZ{}.  \mforall{}d:\mBbbN{}\msupplus{}.    (((r(z)/r(d))  \mmember{}  I)  {}\mRightarrow{}  (f((r(z)/r(d)))  =  g((r(z)/r(d))))))
                {}\mRightarrow{}  (\mforall{}a:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f(a)  =  g(a))))))


By

---

Latex:
(Auto
  THEN  InstLemma  `functions-equal-on-dense`
    [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}r.\mexists{}z:\mBbbZ{}.  \mexists{}d:\mBbbN{}\msupplus{}.  (r  =  (r(z)/r(d)))\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index