---

Step * 1 of Lemma derivative_unique


1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. d(f[x])/dx = λx.g1[x] on I
7. d(f[x])/dx = λx.g2[x] on I
8. x : {x:ℝ| x ∈ I} 
9. m : ℕ+
⊢ |g1(x) - g2(x)| ≤ (r1/r(m))
BY
{ (D -2
   THEN (Unhide THENA Auto)
   THEN DupHyp (-2)
   THEN (RWO "i-member-proper-iff" (-1) THENA Auto)
   THEN ExRepD
   THEN (FLemma `i-approx-compact` [-1] THENA Auto)) }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. d(f[x])/dx = λx.g1[x] on I
7. d(f[x])/dx = λx.g2[x] on I
8. x : ℝ
9. x ∈ I
10. m : ℕ+
11. n : ℕ+
12. iproper(i-approx(I;n))
13. x ∈ i-approx(I;n)
14. icompact(i-approx(I;n))
⊢ |g1(x) - g2(x)| ≤ (r1/r(m))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  iproper(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  g1  :  I  {}\mrightarrow{}\mBbbR{}
5.  g2  :  I  {}\mrightarrow{}\mBbbR{}
6.  d(f[x])/dx  =  \mlambda{}x.g1[x]  on  I
7.  d(f[x])/dx  =  \mlambda{}x.g2[x]  on  I
8.  x  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
9.  m  :  \mBbbN{}\msupplus{}
\mvdash{}  |g1(x)  -  g2(x)|  \mleq{}  (r1/r(m))


By

---

Latex:
(D  -2
  THEN  (Unhide  THENA  Auto)
  THEN  DupHyp  (-2)
  THEN  (RWO  "i-member-proper-iff"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (FLemma  `i-approx-compact`  [-1]  THENA  Auto))

---

Home Index