---

Step * 1 of Lemma continuous-minus


1. I : Interval
2. f : I ⟶ℝ
3. m : {m:ℕ+| icompact(i-approx(I;m))} @i
4. n : ℕ+@i
5. d : ℝ
6. r0 < d
7. r0 < d
8. x : ℝ@i
9. y : ℝ@i
10. x ∈ i-approx(I;m)@i
11. y ∈ i-approx(I;m)@i
12. |x - y| ≤ d@i
13. |f[x] - f[y]| ≤ (r1/r(n))
⊢ |-(f[x]) - -(f[y])| ≤ (r1/r(n))
BY
{ (∀h:hyp. (FLemma `i-member-approx` [h] THENA Complete (Auto)) 
   THEN RWO "rabs-rminus<" (-3)
   THEN Auto
   THEN nRNorm (-3)
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}  @i
4.  n  :  \mBbbN{}\msupplus{}@i
5.  d  :  \mBbbR{}
6.  r0  <  d
7.  r0  <  d
8.  x  :  \mBbbR{}@i
9.  y  :  \mBbbR{}@i
10.  x  \mmember{}  i-approx(I;m)@i
11.  y  \mmember{}  i-approx(I;m)@i
12.  |x  -  y|  \mleq{}  d@i
13.  |f[x]  -  f[y]|  \mleq{}  (r1/r(n))
\mvdash{}  |-(f[x])  -  -(f[y])|  \mleq{}  (r1/r(n))


By

---

Latex:
(\mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THENA  Complete  (Auto)) 
  THEN  RWO  "rabs-rminus<"  (-3)
  THEN  Auto
  THEN  nRNorm  (-3)
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index