---

Step * 1 1 1 1 1 of Lemma differentiable-continuous


1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. ∀k:ℕ+. ∀n:{n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(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|)))))])
6. g[x] (proper)continuous for x ∈ I
7. m : {m:ℕ+| icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m))} 
8. n : ℕ+
9. i-approx(I;m) ⊆ I 
10. M : ℕ+
11. |g x|(x∈i-approx(I;m)) ≤ r(M)
12. ∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|g[x] * (y - x)| ≤ (r(M) * |y - x|)))
13. del : ℝ
14. [%18] : (r0 < del)
∧ (∀x,y:ℝ.
     ((x ∈ i-approx(I;m))
     ⇒ (y ∈ i-approx(I;m))
     ⇒ (|y - x| ≤ del)
     ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r1) * |y - x|))))
15. ∀y,x:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ del) ⇒ (|f[x] - f[y]| ≤ (r(M + 1) * |y - x|)))
⊢ ∃d:ℝ [((r0 < d)
       ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))]
BY
{ xxx(With ⌜rmin(del;(r1/r(n * (M + 1))))⌝ (D 0)⋅ THEN Auto THEN Try ((BLemma `rmin_strict_ub` THEN Auto)))xxx }

1
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. ∀k:ℕ+. ∀n:{n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(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|)))))])
6. g[x] (proper)continuous for x ∈ I
7. m : {m:ℕ+| icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m))} 
8. n : ℕ+
9. i-approx(I;m) ⊆ I 
10. M : ℕ+
11. |g x|(x∈i-approx(I;m)) ≤ r(M)
12. ∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|g[x] * (y - x)| ≤ (r(M) * |y - x|)))
13. del : ℝ
14. r0 < del
15. ∀x,y:ℝ.
      ((x ∈ i-approx(I;m))
      ⇒ (y ∈ i-approx(I;m))
      ⇒ (|y - x| ≤ del)
      ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r1) * |y - x|)))
16. ∀y,x:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ del) ⇒ (|f[x] - f[y]| ≤ (r(M + 1) * |y - x|)))
17. r0 < rmin(del;(r1/r(n * (M + 1))))
18. x : ℝ
19. y : ℝ
20. x ∈ i-approx(I;m)
21. y ∈ i-approx(I;m)
22. |x - y| ≤ rmin(del;(r1/r(n * (M + 1))))
⊢ |f[x] - f[y]| ≤ (r1/r(n))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  g  :  I  {}\mrightarrow{}\mBbbR{}
4.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y]))
5.  \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}n:\{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))\}  .
          (\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{}  (|f[y]  -  f[x]  -  g[x]  *  (y  -  x)|  \mleq{}  ((r1/r(k))  *  |y  -  x|)))))])
6.  g[x]  (proper)continuous  for  x  \mmember{}  I
7.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))  \mwedge{}  iproper(i-approx(I;m))\} 
8.  n  :  \mBbbN{}\msupplus{}
9.  i-approx(I;m)  \msubseteq{}  I 
10.  M  :  \mBbbN{}\msupplus{}
11.  |g  x|(x\mmember{}i-approx(I;m))  \mleq{}  r(M)
12.  \mforall{}x,y:\mBbbR{}.    ((x  \mmember{}  i-approx(I;m))  {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))  {}\mRightarrow{}  (|g[x]  *  (y  -  x)|  \mleq{}  (r(M)  *  |y  -  x|)))
13.  del  :  \mBbbR{}
14.  [\%18]  :  (r0  <  del)
\mwedge{}  (\mforall{}x,y:\mBbbR{}.
          ((x  \mmember{}  i-approx(I;m))
          {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
          {}\mRightarrow{}  (|y  -  x|  \mleq{}  del)
          {}\mRightarrow{}  (|f[y]  -  f[x]  -  g[x]  *  (y  -  x)|  \mleq{}  ((r1/r1)  *  |y  -  x|))))
15.  \mforall{}y,x:\mBbbR{}.
            ((x  \mmember{}  i-approx(I;m))
            {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
            {}\mRightarrow{}  (|x  -  y|  \mleq{}  del)
            {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r(M  +  1)  *  |y  -  x|)))
\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{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(n))))))]


By

---

Latex:
xxx(With  \mkleeneopen{}rmin(del;(r1/r(n  *  (M  +  1))))\mkleeneclose{}  (D  0)\mcdot{}
        THEN  Auto
        THEN  Try  ((BLemma  `rmin\_strict\_ub`  THEN  Auto)))xxx

---

Home Index