---

Step * 1 of Lemma chain-rule


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index