---

Step * 1 1 of Lemma derivative_functionality_wrt_subinterval


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))
BY
{ RepeatFor 2 (ParallelOp 9) }

1
.....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))

2
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))
14. left-endpoint(i-approx(J;n)) < right-endpoint(i-approx(J;n))
⊢ left-endpoint(i-approx(I;m)) < right-endpoint(i-approx(I;m))

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  2  (ParallelOp  9)

---

Home Index