---

Step * 1 of Lemma derivative-continuous


1. I : Interval@i
2. f : I ⟶ℝ@i
3. g : I ⟶ℝ@i
4. ∀x,y:{x:ℝ| x ∈ I} .  (g[x] ≠ g[y] ⇒ x ≠ y)@i
5. λx.g[x] = d(f[x])/dx on I@i
6. m : {m:ℕ+| icompact(i-approx(I;m))} @i
7. n : ℕ+@i
⊢ ∃d:{ℝ| ((r0 < d)
         ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))))}
BY
{ ((InstLemma `i-approx-is-subinterval` [⌜I⌝;⌜m⌝]⋅ THENA Auto)
   THEN Unfold `derivative` 5
   THEN (InstHyp [⌜2 * n⌝;⌜m⌝] 5⋅ THENA Auto)
   THEN (ParallelLast THENA Auto)) }

1
1. I : Interval@i
2. f : I ⟶ℝ@i
3. g : I ⟶ℝ@i
4. ∀x,y:{x:ℝ| x ∈ I} .  (g[x] ≠ g[y] ⇒ x ≠ y)@i
5. ∀k:ℕ+. ∀n:{n:ℕ+| icompact(i-approx(I;n))} .
     (∃del:{ℝ| ((r0 < del)
               ∧ (∀x,y:ℝ.
                    ((x ∈ i-approx(I;n))
                    ⇒ (y ∈ i-approx(I;n))
                    ⇒ (|y - x| ≤ del)
                    ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))})@i
6. m : {m:ℕ+| icompact(i-approx(I;m))} @i
7. n : ℕ+@i
8. i-approx(I;m) ⊆ I 
9. del : ℝ
10. r0 < del
11. ∀x,y:ℝ.
      ((x ∈ i-approx(I;m))
      ⇒ (y ∈ i-approx(I;m))
      ⇒ (|y - x| ≤ del)
      ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(2 * n)) * |y - x|)))
12. r0 < del
13. x : ℝ@i
14. y : ℝ@i
15. x ∈ i-approx(I;m)@i
16. y ∈ i-approx(I;m)@i
17. |x - y| ≤ del@i
⊢ |g[x] - g[y]| ≤ (r1/r(n))

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  f  :  I  {}\mrightarrow{}\mBbbR{}@i
3.  g  :  I  {}\mrightarrow{}\mBbbR{}@i
4.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (g[x]  \mneq{}  g[y]  {}\mRightarrow{}  x  \mneq{}  y)@i
5.  \mlambda{}x.g[x]  =  d(f[x])/dx  on  I@i
6.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}  @i
7.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  \mexists{}d:\{\mBbbR{}|  ((r0  <  d)
                  \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                            ((x  \mmember{}  i-approx(I;m))
                            {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
                            {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
                            {}\mRightarrow{}  (|g[x]  -  g[y]|  \mleq{}  (r1/r(n))))))\}


By

---

Latex:
((InstLemma  `i-approx-is-subinterval`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `derivative`  5
  THEN  (InstHyp  [\mkleeneopen{}2  *  n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  (ParallelLast  THENA  Auto))

---

Home Index