---

Step * 1 of Lemma derivative_functionality_wrt_subinterval

.....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))} 
BY
{ (DSetVars THEN MemTypeCD THEN Auto) }

1
1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. J ⊆ I 
6. k : ℕ+
7. n : ℕ+
8. icompact(i-approx(J;n))
9. iproper(i-approx(J;n))
10. m : ℕ+
11. icompact(i-approx(I;m))
12. i-approx(J;n) ⊆ i-approx(I;m) 
13. icompact(i-approx(I;m))
⊢ iproper(i-approx(I;m))

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  Interval
2.  J  :  Interval
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  f'  :  I  {}\mrightarrow{}\mBbbR{}
5.  J  \msubseteq{}  I 
6.  k  :  \mBbbN{}\msupplus{}
7.  n  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(J;n))  \mwedge{}  iproper(i-approx(J;n))\} 
8.  m  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))\} 
9.  i-approx(J;n)  \msubseteq{}  i-approx(I;m) 
\mvdash{}  m  \mmember{}  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))\} 


By

---

Latex:
(DSetVars  THEN  MemTypeCD  THEN  Auto)

---

Home Index