---

Step * of Lemma continuous_functionality_wrt_rfun-eq

∀I:Interval. ∀[f1,f2:I ⟶ℝ].  (rfun-eq(I;λx.f1[x];λx.f2[x]) ⇒ f1[x] continuous for x ∈ I ⇒ f2[x] continuous for x ∈ I)
BY
{ (Auto
   THEN RepeatFor 4 (ParallelLast')
   THEN Try (OnMaybeHyp 11 (\h. (FLemma `i-member-approx` [h] THEN Complete (Auto)))⋅)
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))⋅) }

1
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))

---

Latex:

---

Latex:
\mforall{}I:Interval
    \mforall{}[f1,f2:I  {}\mrightarrow{}\mBbbR{}].
        (rfun-eq(I;\mlambda{}x.f1[x];\mlambda{}x.f2[x])  {}\mRightarrow{}  f1[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  f2[x]  continuous  for  x  \mmember{}  I)


By

---

Latex:
(Auto
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Try  (OnMaybeHyp  11  (\mbackslash{}h.  (FLemma  `i-member-approx`  [h]  THEN  Complete  (Auto)))\mcdot{})
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))\mcdot{})

---

Home Index