---

Step * 1 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 : ℝ
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))
BY
{ (∀h:hyp. (UnfoldTop `derivative` h
            THEN (InstHyp [⌜2 * m⌝;⌜n⌝] h⋅ THENA Complete (Auto))
            THEN Thin h
            THEN D -1
            THEN (Unhide THENA Auto)) 
   THEN Auto
   ) }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. x : ℝ
7. x ∈ I
8. m : ℕ+
9. n : ℕ+
10. iproper(i-approx(I;n))
11. x ∈ i-approx(I;n)
12. icompact(i-approx(I;n))
13. del : ℝ
14. r0 < del
15. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|y - x| ≤ del)
      ⇒ (|f[y] - f[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)))
16. d1 : ℝ
17. r0 < d1
18. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|y - x| ≤ d1)
      ⇒ (|f[y] - f[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)))
⊢ |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  :  \mBbbR{}
9.  x  \mmember{}  I
10.  m  :  \mBbbN{}\msupplus{}
11.  n  :  \mBbbN{}\msupplus{}
12.  iproper(i-approx(I;n))
13.  x  \mmember{}  i-approx(I;n)
14.  icompact(i-approx(I;n))
\mvdash{}  |g1(x)  -  g2(x)|  \mleq{}  (r1/r(m))


By

---

Latex:
(\mforall{}h:hyp.  (UnfoldTop  `derivative`  h
                    THEN  (InstHyp  [\mkleeneopen{}2  *  m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto))
                    THEN  Thin  h
                    THEN  D  -1
                    THEN  (Unhide  THENA  Auto)) 
  THEN  Auto
  )

---

Home Index