---

Step * 1 1 2 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. 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))
15. ∀[r:ℝ]. left-endpoint(i-approx(I;m))≤r≤right-endpoint(i-approx(I;m)) supposing r ∈ i-approx(I;m)
⊢ left-endpoint(i-approx(I;m)) < right-endpoint(i-approx(I;m))
BY
{ (InstHyp [⌜left-endpoint(i-approx(J;n))⌝] (-1)⋅ THENA Auto) }

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))
14. left-endpoint(i-approx(J;n)) < right-endpoint(i-approx(J;n))
15. ∀[r:ℝ]. left-endpoint(i-approx(I;m))≤r≤right-endpoint(i-approx(I;m)) supposing r ∈ i-approx(I;m)
⊢ left-endpoint(i-approx(J;n)) ∈ i-approx(I;m)

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))
15. ∀[r:ℝ]. left-endpoint(i-approx(I;m))≤r≤right-endpoint(i-approx(I;m)) supposing r ∈ i-approx(I;m)
16. left-endpoint(i-approx(I;m))≤left-endpoint(i-approx(J;n))≤right-endpoint(i-approx(I;m))
⊢ 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.  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))
14.  left-endpoint(i-approx(J;n))  <  right-endpoint(i-approx(J;n))
15.  \mforall{}[r:\mBbbR{}].  left-endpoint(i-approx(I;m))\mleq{}r\mleq{}right-endpoint(i-approx(I;m))  supposing  r  \mmember{}  i-approx(I;m)
\mvdash{}  left-endpoint(i-approx(I;m))  <  right-endpoint(i-approx(I;m))


By

---

Latex:
(InstHyp  [\mkleeneopen{}left-endpoint(i-approx(J;n))\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)

---

Home Index