---

Step * of Lemma differentiable-functional2

∀I:Interval. ∀f,g:I ⟶ℝ.
  ((∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y])))
  ⇒ d(f[x])/dx = λx.g[x] on I
  ⇒ iproper(I)
  ⇒ (∀a,b:{x:ℝ| x ∈ I} .  ((a = b) ⇒ (f[a] = f[b]))))
BY
{ xxx(InstLemma `differentiable-continuous` []
      THEN RepeatFor 5 ((ParallelLast' THENA Auto))
      THEN Auto
      THEN InstLemma `proper-continuous-implies-functional` [⌜I⌝;⌜f⌝]⋅
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f,g:I  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y])))
    {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
    {}\mRightarrow{}  iproper(I)
    {}\mRightarrow{}  (\mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((a  =  b)  {}\mRightarrow{}  (f[a]  =  f[b]))))


By

---

Latex:
xxx(InstLemma  `differentiable-continuous`  []
        THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))
        THEN  Auto
        THEN  InstLemma  `proper-continuous-implies-functional`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
        THEN  Auto)xxx

---

Home Index