---

Step * 1 1 of Lemma simple-chain-rule


1. I : Interval
2. ∀J:Interval. ∀f,f':I ⟶ℝ. ∀g,g':J ⟶ℝ.
     (iproper(J)
     ⇒ maps-compact(I;J;x.f[x])
     ⇒ (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f'[x] = f'[y])))
     ⇒ (∀x,y:{x:ℝ| x ∈ J} .  ((x = y) ⇒ (g'[x] = g'[y])))
     ⇒ d(f[x])/dx = λx.f'[x] on I
     ⇒ d(g[x])/dx = λx.g'[x] on J
     ⇒ d(g[f[x]])/dx = λx.g'[f[x]] * f'[x] on I)
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. g : (-∞, ∞) ⟶ℝ
6. g' : (-∞, ∞) ⟶ℝ
7. iproper((-∞, ∞))
⇒ maps-compact(I;(-∞, ∞);x.f[x])
⇒ (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f'[x] = f'[y])))
⇒ (∀x,y:{x:ℝ| x ∈ (-∞, ∞)} .  ((x = y) ⇒ (g'[x] = g'[y])))
⇒ d(f[x])/dx = λx.f'[x] on I
⇒ d(g[x])/dx = λx.g'[x] on (-∞, ∞)
⇒ d(g[f[x]])/dx = λx.g'[f[x]] * f'[x] on I
8. iproper(I)
9. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f'[x] = f'[y]))
10. ∀x,y:ℝ.  ((x = y) ⇒ (g'[x] = g'[y]))
11. d(f[x])/dx = λx.f'[x] on I
12. d(g[x])/dx = λx.g'[x] on (-∞, ∞)
⊢ f[x] (proper)continuous for x ∈ I
BY
{ (FLemma `differentiable-continuous` [-2] THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  \mforall{}J:Interval.  \mforall{}f,f':I  {}\mrightarrow{}\mBbbR{}.  \mforall{}g,g':J  {}\mrightarrow{}\mBbbR{}.
          (iproper(J)
          {}\mRightarrow{}  maps-compact(I;J;x.f[x])
          {}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y])))
          {}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  J\}  .    ((x  =  y)  {}\mRightarrow{}  (g'[x]  =  g'[y])))
          {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
          {}\mRightarrow{}  d(g[x])/dx  =  \mlambda{}x.g'[x]  on  J
          {}\mRightarrow{}  d(g[f[x]])/dx  =  \mlambda{}x.g'[f[x]]  *  f'[x]  on  I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  f'  :  I  {}\mrightarrow{}\mBbbR{}
5.  g  :  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
6.  g'  :  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
7.  iproper((-\minfty{},  \minfty{}))
{}\mRightarrow{}  maps-compact(I;(-\minfty{},  \minfty{});x.f[x])
{}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y])))
{}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  (-\minfty{},  \minfty{})\}  .    ((x  =  y)  {}\mRightarrow{}  (g'[x]  =  g'[y])))
{}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
{}\mRightarrow{}  d(g[x])/dx  =  \mlambda{}x.g'[x]  on  (-\minfty{},  \minfty{})
{}\mRightarrow{}  d(g[f[x]])/dx  =  \mlambda{}x.g'[f[x]]  *  f'[x]  on  I
8.  iproper(I)
9.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y]))
10.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (g'[x]  =  g'[y]))
11.  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
12.  d(g[x])/dx  =  \mlambda{}x.g'[x]  on  (-\minfty{},  \minfty{})
\mvdash{}  f[x]  (proper)continuous  for  x  \mmember{}  I


By

---

Latex:
(FLemma  `differentiable-continuous`  [-2]  THEN  Try  (Complete  (Auto)))

---

Home Index