---

Step * 1 2 1 1 1 of Lemma derivative-of-integral

.....wf..... 
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))
7. ∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (|a_∫-y f[t] dt - a_∫-x f[t] dt - f[x] * (y - x)| = |x_∫-y f[t] - f[x] dt|))
8. i-approx(I;n) ⊆ I 
⊢ λx.f[x] ∈ {f:i-approx(I;n) ⟶ℝ| ifun(f;i-approx(I;n))} 
BY
{ (DVar `f' THEN Unfold `so_apply` 0 THEN MemTypeCD THEN Auto) }

1
1. I : Interval
2. a : {a:ℝ| a ∈ I} 
3. f : I ⟶ℝ
4. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))
5. k : ℕ+
6. n : ℕ+
7. icompact(i-approx(I;n))
8. iproper(i-approx(I;n))
9. ∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (|a_∫-y f[t] dt - a_∫-x f[t] dt - f[x] * (y - x)| = |x_∫-y f[t] - f[x] dt|))
10. i-approx(I;n) ⊆ I 
⊢ ifun(λx.(f x);i-approx(I;n))

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  Interval
2.  a  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
3.  f  :  \{f:I  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))\} 
4.  k  :  \mBbbN{}\msupplus{}
5.  n  :  \mBbbN{}\msupplus{}
6.  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))
7.  \mforall{}x,y:\mBbbR{}.
          ((x  \mmember{}  I)
          {}\mRightarrow{}  (y  \mmember{}  I)
          {}\mRightarrow{}  (|a\_\mint{}\msupminus{}y  f[t]  dt  -  a\_\mint{}\msupminus{}x  f[t]  dt  -  f[x]  *  (y  -  x)|  =  |x\_\mint{}\msupminus{}y  f[t]  -  f[x]  dt|))
8.  i-approx(I;n)  \msubseteq{}  I 
\mvdash{}  \mlambda{}x.f[x]  \mmember{}  \{f:i-approx(I;n)  {}\mrightarrow{}\mBbbR{}|  ifun(f;i-approx(I;n))\} 


By

---

Latex:
(DVar  `f'  THEN  Unfold  `so\_apply`  0  THEN  MemTypeCD  THEN  Auto)

---

Home Index