---

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


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))
BY
{ ((FLemma `icompact-is-rccint` [-4] THENA Auto) THEN RWO "-1" (-2)) }

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. [left-endpoint(i-approx(I;n)), right-endpoint(i-approx(I;n))] ⊆ I 
11. i-approx(I;n) ~ [left-endpoint(i-approx(I;n)), right-endpoint(i-approx(I;n))]
⊢ ifun(λx.(f x);i-approx(I;n))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  a  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))
5.  k  :  \mBbbN{}\msupplus{}
6.  n  :  \mBbbN{}\msupplus{}
7.  icompact(i-approx(I;n))
8.  iproper(i-approx(I;n))
9.  \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|))
10.  i-approx(I;n)  \msubseteq{}  I 
\mvdash{}  ifun(\mlambda{}x.(f  x);i-approx(I;n))


By

---

Latex:
((FLemma  `icompact-is-rccint`  [-4]  THENA  Auto)  THEN  RWO  "-1"  (-2))

---

Home Index