---

Step * of Lemma derivative_unique

∀[I:Interval]
  (iproper(I) ⇒ (∀[f,g1,g2:I ⟶ℝ].  (d(f[x])/dx = λx.g1[x] on I ⇒ d(f[x])/dx = λx.g2[x] on I ⇒ rfun-eq(I;g1;g2))))
BY
{ (Auto THEN (D 0 THENA Auto) THEN BLemma `req-iff-rabs-rleq` THEN 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 : {x:ℝ| x ∈ I} 
9. m : ℕ+
⊢ |g1(x) - g2(x)| ≤ (r1/r(m))

---

Latex:

---

Latex:
\mforall{}[I:Interval]
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}[f,g1,g2:I  {}\mrightarrow{}\mBbbR{}].
                (d(f[x])/dx  =  \mlambda{}x.g1[x]  on  I  {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.g2[x]  on  I  {}\mRightarrow{}  rfun-eq(I;g1;g2))))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  BLemma  `req-iff-rabs-rleq`  THEN  Auto)

---

Home Index