---

Step * of Lemma mean-value-for-bounded-derivative

∀I:Interval
  (iproper(I)
  ⇒ (∀f,f':I ⟶ℝ.
        ((∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f'[x] = f'[y])))
        ⇒ d(f[x])/dx = λx.f'[x] on I
        ⇒ (∀c:ℝ. ((∀x:{x:ℝ| x ∈ I} . (|f'[x]| ≤ c)) ⇒ (∀x,y:{x:ℝ| x ∈ I} .  (|f[x] - f[y]| ≤ (c * |x - y|))))))))
BY
{ (Auto
   THEN ((InstLemma `function-is-continuous` [⌜I⌝;⌜f'⌝]⋅ THENA Auto)
         THEN (Assert f[x] continuous for x ∈ I BY
                     ((FLemma `differentiable-continuous` [6] THENA Auto)
                      THEN FLemma `proper-continuous-is-continuous` [-1]
                      THEN Auto))
         )
   THEN BLemma `rleq-iff-all-rless`
   THEN Auto) }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f'[x] = f'[y]))
6. d(f[x])/dx = λx.f'[x] on I
7. c : ℝ
8. ∀x:{x:ℝ| x ∈ I} . (|f'[x]| ≤ c)
9. x : {x:ℝ| x ∈ I} 
10. y : {x:ℝ| x ∈ I} 
11. f'[x] continuous for x ∈ I
12. f[x] continuous for x ∈ I
13. e : {e:ℝ| r0 < e} 
⊢ |f[x] - f[y]| ≤ ((c * |x - y|) + e)

---

Latex:

---

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}f,f':I  {}\mrightarrow{}\mBbbR{}.
                ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y])))
                {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
                {}\mRightarrow{}  (\mforall{}c:\mBbbR{}
                            ((\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (|f'[x]|  \mleq{}  c))
                            {}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (|f[x]  -  f[y]|  \mleq{}  (c  *  |x  -  y|))))))))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `function-is-continuous`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (Assert  f[x]  continuous  for  x  \mmember{}  I  BY
                                      ((FLemma  `differentiable-continuous`  [6]  THENA  Auto)
                                        THEN  FLemma  `proper-continuous-is-continuous`  [-1]
                                        THEN  Auto))
              )
  THEN  BLemma  `rleq-iff-all-rless`
  THEN  Auto)

---

Home Index