---

Step * 1 1 1 of Lemma chain-rule_0


1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. g : J ⟶ℝ
6. g' : J ⟶ℝ
7. f[x] (proper)continuous for x ∈ I
8. f'[x] (proper)continuous for x ∈ I
9. g'[x] (proper)continuous for x ∈ J
10. d(f[x])/dx = λx.f'[x] on I
11. d(g[x])/dx = λx.g'[x] on J
12. k : ℕ+
13. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
14. m : {m:ℕ+| icompact(i-approx(J;m)) ∧ iproper(i-approx(J;m))} 
15. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))
16. iproper(i-approx(I;n))
17. mc1 : f'[x] continuous for x ∈ i-approx(I;n)
18. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f'[x]| ≤ a)
⊢ ∃del:ℝ [((r0 < del)
         ∧ (∀x,y:ℝ.
              ((x ∈ i-approx(I;n))
              ⇒ (y ∈ i-approx(I;n))
              ⇒ (|y - x| ≤ del)
              ⇒ (|g[f[y]] - g[f[x]] - (g'[f[x]] * f'[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))]
BY
{ ((Assert iproper(i-approx(J;m)) BY
          (DVar `m' THEN (Unhide THEN Auto) THEN Unfold `iproper` 0 THEN Auto))
   THEN (InstLemma `proper-continuous-implies` [⌜J⌝;⌜g'⌝;⌜m⌝] ⋅ THENA Auto)
   THEN (RenameVar `mc2' (-1)
         THEN (Assert ∃b:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(J;m)} ]. (|g'[x]| ≤ b) BY
                     ((InstLemma `Inorm-bound` [⌜i-approx(J;m)⌝;⌜g'⌝;⌜mc2⌝]⋅ THENA Auto)
                      THEN (InstLemma `Inorm_wf` [⌜i-approx(J;m)⌝;⌜g'⌝;⌜mc2⌝]⋅ THENA Auto)
                      THEN With ⌜||g'[x]||_i-approx(J;m)⌝ (D 0)⋅
                      THEN Auto
                      THEN DSetVars
                      THEN FLemma `i-member-approx` [-1]
                      THEN Auto))
         )⋅) }

1
1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. g : J ⟶ℝ
6. g' : J ⟶ℝ
7. f[x] (proper)continuous for x ∈ I
8. f'[x] (proper)continuous for x ∈ I
9. g'[x] (proper)continuous for x ∈ J
10. d(f[x])/dx = λx.f'[x] on I
11. d(g[x])/dx = λx.g'[x] on J
12. k : ℕ+
13. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
14. m : {m:ℕ+| icompact(i-approx(J;m)) ∧ iproper(i-approx(J;m))} 
15. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))
16. iproper(i-approx(I;n))
17. mc1 : f'[x] continuous for x ∈ i-approx(I;n)
18. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f'[x]| ≤ a)
19. iproper(i-approx(J;m))
20. mc2 : g'[x] continuous for x ∈ i-approx(J;m)
21. ∃b:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(J;m)} ]. (|g'[x]| ≤ b)
⊢ ∃del:ℝ [((r0 < del)
         ∧ (∀x,y:ℝ.
              ((x ∈ i-approx(I;n))
              ⇒ (y ∈ i-approx(I;n))
              ⇒ (|y - x| ≤ del)
              ⇒ (|g[f[y]] - g[f[x]] - (g'[f[x]] * f'[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))]

---

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.  f[x]  (proper)continuous  for  x  \mmember{}  I
8.  f'[x]  (proper)continuous  for  x  \mmember{}  I
9.  g'[x]  (proper)continuous  for  x  \mmember{}  J
10.  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
11.  d(g[x])/dx  =  \mlambda{}x.g'[x]  on  J
12.  k  :  \mBbbN{}\msupplus{}
13.  n  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))\} 
14.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(J;m))  \mwedge{}  iproper(i-approx(J;m))\} 
15.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;n)\}  .  (f[x]  \mmember{}  i-approx(J;m))
16.  iproper(i-approx(I;n))
17.  mc1  :  f'[x]  continuous  for  x  \mmember{}  i-approx(I;n)
18.  \mexists{}a:\mBbbR{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|f'[x]|  \mleq{}  a)
\mvdash{}  \mexists{}del:\mBbbR{}  [((r0  <  del)
                  \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                            ((x  \mmember{}  i-approx(I;n))
                            {}\mRightarrow{}  (y  \mmember{}  i-approx(I;n))
                            {}\mRightarrow{}  (|y  -  x|  \mleq{}  del)
                            {}\mRightarrow{}  (|g[f[y]]  -  g[f[x]]  -  (g'[f[x]]  *  f'[x])  *  (y  -  x)|  \mleq{}  ((r1/r(k))  *  |y  -  x|)))))]


By

---

Latex:
((Assert  iproper(i-approx(J;m))  BY
                (DVar  `m'  THEN  (Unhide  THEN  Auto)  THEN  Unfold  `iproper`  0  THEN  Auto))
  THEN  (InstLemma  `proper-continuous-implies`  [\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  \mcdot{}  THENA  Auto)
  THEN  (RenameVar  `mc2'  (-1)
              THEN  (Assert  \mexists{}b:\mBbbR{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(J;m)\}  ].  (|g'[x]|  \mleq{}  b)  BY
                                      ((InstLemma  `Inorm-bound`  [\mkleeneopen{}i-approx(J;m)\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{};\mkleeneopen{}mc2\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                        THEN  (InstLemma  `Inorm\_wf`  [\mkleeneopen{}i-approx(J;m)\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{};\mkleeneopen{}mc2\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                        THEN  With  \mkleeneopen{}||g'[x]||\_i-approx(J;m)\mkleeneclose{}  (D  0)\mcdot{}
                                        THEN  Auto
                                        THEN  DSetVars
                                        THEN  FLemma  `i-member-approx`  [-1]
                                        THEN  Auto))
              )\mcdot{})

---

Home Index