---

Step * 1 1 1 1 2 1 of Lemma derivative-continuous


1. I : Interval@i
2. g : I ⟶ℝ@i
3. ∀x,y:{x:ℝ| x ∈ I} .  (g[x] ≠ g[y] ⇒ x ≠ y)@i
4. m : {m:ℕ+| icompact(i-approx(I;m))} @i
5. n : ℕ+@i
6. i-approx(I;m) ⊆ I 
7. del : ℝ
8. r0 < del
9. r0 < del
10. x : ℝ@i
11. y : ℝ@i
12. x ∈ i-approx(I;m)@i
13. y ∈ i-approx(I;m)@i
14. |x - y| ≤ del@i
15. (|g[x] - g[y]| * |x - y|) ≤ ((r1/r(n)) * |x - y|)
⊢ |g[x] - g[y]| ≤ (r1/r(n))
BY
{ ((BLemma `rleq-iff-not-rless` THENA Auto) THEN (D 0 THENA Auto)) }

1
1. I : Interval@i
2. g : I ⟶ℝ@i
3. ∀x,y:{x:ℝ| x ∈ I} .  (g[x] ≠ g[y] ⇒ x ≠ y)@i
4. m : {m:ℕ+| icompact(i-approx(I;m))} @i
5. n : ℕ+@i
6. i-approx(I;m) ⊆ I 
7. del : ℝ
8. r0 < del
9. r0 < del
10. x : ℝ@i
11. y : ℝ@i
12. x ∈ i-approx(I;m)@i
13. y ∈ i-approx(I;m)@i
14. |x - y| ≤ del@i
15. (|g[x] - g[y]| * |x - y|) ≤ ((r1/r(n)) * |x - y|)
16. (r1/r(n)) < |g[x] - g[y]|@i
⊢ False

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  g  :  I  {}\mrightarrow{}\mBbbR{}@i
3.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (g[x]  \mneq{}  g[y]  {}\mRightarrow{}  x  \mneq{}  y)@i
4.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}  @i
5.  n  :  \mBbbN{}\msupplus{}@i
6.  i-approx(I;m)  \msubseteq{}  I 
7.  del  :  \mBbbR{}
8.  r0  <  del
9.  r0  <  del
10.  x  :  \mBbbR{}@i
11.  y  :  \mBbbR{}@i
12.  x  \mmember{}  i-approx(I;m)@i
13.  y  \mmember{}  i-approx(I;m)@i
14.  |x  -  y|  \mleq{}  del@i
15.  (|g[x]  -  g[y]|  *  |x  -  y|)  \mleq{}  ((r1/r(n))  *  |x  -  y|)
\mvdash{}  |g[x]  -  g[y]|  \mleq{}  (r1/r(n))


By

---

Latex:
((BLemma  `rleq-iff-not-rless`  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index