---

Step * 1 1 of Lemma derivative-is-zero

.....assertion..... 
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. d(f[x])/dx = λx.r0 on I
⊢ ∀a,b:{x:ℝ| x ∈ I} .  ((a < b) ⇒ (f[a] = f[b]))
BY
{ (Auto THEN BLemma `req-iff-rabs-rleq` THEN Auto) }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. d(f[x])/dx = λx.r0 on I
5. a : {x:ℝ| x ∈ I} 
6. b : {x:ℝ| x ∈ I} 
7. a < b
8. m : ℕ+
⊢ |f[a] - f[b]| ≤ (r1/r(m))

---

Latex:

---

Latex:
.....assertion..... 
1.  I  :  Interval
2.  iproper(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  d(f[x])/dx  =  \mlambda{}x.r0  on  I
\mvdash{}  \mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((a  <  b)  {}\mRightarrow{}  (f[a]  =  f[b]))


By

---

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

---

Home Index