---

Step * 1 1 1 of Lemma derivative_functionality_wrt_subinterval

.....antecedent..... 
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. m : ℕ+
10. icompact(i-approx(I;m))
11. i-approx(J;n) ⊆ i-approx(I;m) 
12. icompact(i-approx(I;m))
13. i-finite(i-approx(I;m))
⊢ i-finite(i-approx(J;n))
BY
{ (FLemma `i-finite-subinterval` [-3] THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
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  :  \mBbbN{}\msupplus{}
8.  icompact(i-approx(J;n))
9.  m  :  \mBbbN{}\msupplus{}
10.  icompact(i-approx(I;m))
11.  i-approx(J;n)  \msubseteq{}  i-approx(I;m) 
12.  icompact(i-approx(I;m))
13.  i-finite(i-approx(I;m))
\mvdash{}  i-finite(i-approx(J;n))


By

---

Latex:
(FLemma  `i-finite-subinterval`  [-3]  THEN  Auto)

---

Home Index