---

Step * of Lemma derivative-of-integral

∀I:Interval. ∀a:{a:ℝ| a ∈ I} . ∀f:{f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))} .
  d(a_∫-x f[t] dt)/dx = λt.f[t] on I
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (Assert icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n)) BY
               (D -1 THEN Unhide THEN Auto THEN Unfold `iproper` 0 THEN Auto))
   THEN D -2
   THEN Thin (-2)) }

1
1. I : Interval
2. a : {a:ℝ| a ∈ I} 
3. f : {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))} 
4. k : ℕ+
5. n : ℕ+
6. 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)
              ⇒ (|a_∫-y f[t] dt - a_∫-x f[t] dt - f[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))]

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}a:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  \mforall{}f:\{f:I  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))\}  .
    d(a\_\mint{}\msupminus{}x  f[t]  dt)/dx  =  \mlambda{}t.f[t]  on  I


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (Assert  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))  BY
                          (D  -1  THEN  Unhide  THEN  Auto  THEN  Unfold  `iproper`  0  THEN  Auto))
  THEN  D  -2
  THEN  Thin  (-2))

---

Home Index