---

Step * of Lemma chain-rule_0

∀I,J:Interval. ∀f,f':I ⟶ℝ. ∀g,g':J ⟶ℝ.
  (iproper(J)
  ⇒ maps-compact(I;J;x.f[x])
  ⇒ 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)
BY
{ (Auto
   THEN (Assert maps-compact-proper(I;J;x.f[x]) BY
               (BLemma `proper-maps-compact` THEN Auto))
   THEN PromoteHyp (-1) 9
   THEN RepeatFor 2 (Thin 7)) }

1
1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. g : J ⟶ℝ
6. g' : J ⟶ℝ
7. maps-compact-proper(I;J;x.f[x])
8. f[x] (proper)continuous for x ∈ I
9. f'[x] (proper)continuous for x ∈ I
10. g'[x] (proper)continuous for x ∈ J
11. d(f[x])/dx = λx.f'[x] on I
12. d(g[x])/dx = λx.g'[x] on J
⊢ d(g[f[x]])/dx = λx.g'[f[x]] * f'[x] on I

---

Latex:

---

Latex:
\mforall{}I,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{}  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)


By

---

Latex:
(Auto
  THEN  (Assert  maps-compact-proper(I;J;x.f[x])  BY
                          (BLemma  `proper-maps-compact`  THEN  Auto))
  THEN  PromoteHyp  (-1)  9
  THEN  RepeatFor  2  (Thin  7))

---

Home Index