---

Step * of Lemma derivative_functionality_wrt_subinterval

∀I,J:Interval.  ∀[f,f':I ⟶ℝ].  (J ⊆ I  ⇒ d(f[x])/dx = λx.f'[x] on I ⇒ d(f[x])/dx = λx.f'[x] on J)
BY
{ (Auto
   THEN RepeatFor 2 ((ParallelLast THENA Auto))
   THEN Auto
   THEN (InstLemma `compact-subinterval` [⌜I⌝;⌜i-approx(J;n)⌝]⋅
         THENA (Auto THEN Using [`J',⌜J⌝] (BLemma `subinterval_transitivity`)⋅ THEN Auto)
         )
   THEN D -1
   THEN RenameVar `m' (-2)
   THEN (With ⌜m⌝ (D 7)⋅ THENA Auto)) }

1
.....wf..... 
1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. J ⊆ I 
6. k : ℕ+
7. n : {n:ℕ+| icompact(i-approx(J;n)) ∧ iproper(i-approx(J;n))} 
8. m : {n:ℕ+| icompact(i-approx(I;n))} 
9. i-approx(J;n) ⊆ i-approx(I;m) 
⊢ m ∈ {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 

2
1. I : Interval
2. J : Interval
3. [f] : I ⟶ℝ
4. [f'] : I ⟶ℝ
5. J ⊆ I 
6. k : ℕ+
7. n : {n:ℕ+| icompact(i-approx(J;n)) ∧ iproper(i-approx(J;n))} 
8. m : {n:ℕ+| icompact(i-approx(I;n))} 
9. i-approx(J;n) ⊆ i-approx(I;m) 
10. ∃del:{ℝ| ((r0 < del)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m))
                  ⇒ (y ∈ i-approx(I;m))
                  ⇒ (|y - x| ≤ del)
                  ⇒ (|f[y] - f[x] - f'[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))}
⊢ ∃del:{ℝ| ((r0 < del)
           ∧ (∀x,y:ℝ.
                ((x ∈ i-approx(J;n))
                ⇒ (y ∈ i-approx(J;n))
                ⇒ (|y - x| ≤ del)
                ⇒ (|f[y] - f[x] - f'[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))}

---

Latex:

---

Latex:
\mforall{}I,J:Interval.    \mforall{}[f,f':I  {}\mrightarrow{}\mBbbR{}].    (J  \msubseteq{}  I    {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I  {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  J)


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((ParallelLast  THENA  Auto))
  THEN  Auto
  THEN  (InstLemma  `compact-subinterval`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}i-approx(J;n)\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Using  [`J',\mkleeneopen{}J\mkleeneclose{}]  (BLemma  `subinterval\_transitivity`)\mcdot{}  THEN  Auto)
              )
  THEN  D  -1
  THEN  RenameVar  `m'  (-2)
  THEN  (With  \mkleeneopen{}m\mkleeneclose{}  (D  7)\mcdot{}  THENA  Auto))

---

Home Index