---

Step * 1 1 2 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))
⊢ left-endpoint(i-approx(I;m)) < right-endpoint(i-approx(I;m))
BY
{ (InstLemma `i-member-finite` [⌜i-approx(I;m)⌝]⋅ THENA 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. 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))

---

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))
\mvdash{}  left-endpoint(i-approx(I;m))  <  right-endpoint(i-approx(I;m))


By

---

Latex:
(InstLemma  `i-member-finite`  [\mkleeneopen{}i-approx(I;m)\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index