---

Step * of Lemma function-diff-small-or-interval-proper

∀I:Interval. ∀f:I ⟶ℝ. ∀x,y:{x:ℝ| x ∈ I} . ∀e:{e:ℝ| r0 < e} .
  (f[x] continuous for x ∈ I ⇒ ((|f[x] - f[y]| ≤ e) ∨ (r0 < |x - y|)))
BY
{ (Auto
   THEN (InstLemma `rmin-rmax-subinterval` [⌜I⌝;⌜x⌝;⌜y⌝]⋅ THENA Auto)
   THEN (FLemma `continuous_functionality_wrt_subinterval` [-2;-1]⋅ THENA Auto)
   THEN (D -1 With ⌜1⌝  THENA Auto)
   THEN All (RepUR ``i-approx``)
   THEN Try ((MemTypeCD THEN Auto))
   THEN (InstLemma `small-reciprocal-real` [⌜e⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (D -3 With ⌜k⌝  THENA Auto)
   THEN ExRepD) }

1
1. I : Interval
2. f : I ⟶ℝ
3. x : {x:ℝ| x ∈ I} 
4. y : {x:ℝ| x ∈ I} 
5. e : {e:ℝ| r0 < e} 
6. f[x] continuous for x ∈ I
7. [rmin(x;y), rmax(x;y)] ⊆ I 
8. k : ℕ+
9. (r1/r(k)) < e
10. d : ℝ
11. r0 < d
12. ∀x@0,y@0:ℝ.
      (((rmin(x;y) ≤ x@0) ∧ (x@0 ≤ rmax(x;y)))
      ⇒ ((rmin(x;y) ≤ y@0) ∧ (y@0 ≤ rmax(x;y)))
      ⇒ (|x@0 - y@0| ≤ d)
      ⇒ (|f[x@0] - f[y@0]| ≤ (r1/r(k))))
⊢ (|f[x] - f[y]| ≤ e) ∨ (r0 < |x - y|)

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
    (f[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  ((|f[x]  -  f[y]|  \mleq{}  e)  \mvee{}  (r0  <  |x  -  y|)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `rmin-rmax-subinterval`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (FLemma  `continuous\_functionality\_wrt\_subinterval`  [-2;-1]\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}1\mkleeneclose{}    THENA  Auto)
  THEN  All  (RepUR  ``i-approx``)
  THEN  Try  ((MemTypeCD  THEN  Auto))
  THEN  (InstLemma  `small-reciprocal-real`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (D  -3  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD)

---

Home Index