---

Step * 1 of Lemma continuous_functionality_wrt_rfun-eq


1. I : Interval@i
2. f1 : I ⟶ℝ
3. f2 : I ⟶ℝ
4. rfun-eq(I;λx.f1[x];λx.f2[x])@i
5. m : {m:ℕ+| icompact(i-approx(I;m))} @i
6. n : ℕ+@i
7. d : ℝ
8. r0 < d
9. x : ℝ@i
10. y : ℝ@i
11. x ∈ i-approx(I;m)@i
12. y ∈ i-approx(I;m)@i
13. |x - y| ≤ d@i
14. |f1[x] - f1[y]| ≤ (r1/r(n))
⊢ |f2[x] - f2[y]| ≤ (r1/r(n))
BY
{ (Unfold `rfun-eq` 4
   THEN RepUR ``r-ap`` 4
   THEN RWO "4" (-1)
   THEN Auto
   THEN Try (OnMaybeHyp 11 (\h. (FLemma `i-member-approx` [h] THEN Complete (Auto)))⋅)) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `rfun-eq`  4
  THEN  RepUR  ``r-ap``  4
  THEN  RWO  "4"  (-1)
  THEN  Auto
  THEN  Try  (OnMaybeHyp  11  (\mbackslash{}h.  (FLemma  `i-member-approx`  [h]  THEN  Complete  (Auto)))\mcdot{}))

---

Home Index