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 ∈  f2[x] continuous for x ∈ I)
BY
(Auto
   THEN RepeatFor (ParallelLast')
   THEN Try (OnMaybeHyp 11 (\h. (FLemma `i-member-approx` [h] THEN Complete (Auto)))⋅)
   THEN RepeatFor ((ParallelLast' THENA Auto))⋅}

1
1. Interval@i
2. f1 I ⟶ℝ
3. f2 I ⟶ℝ
4. rfun-eq(I;λx.f1[x];λx.f2[x])@i
5. {m:ℕ+icompact(i-approx(I;m))} @i
6. : ℕ+@i
7. : ℝ
8. r0 < d
9. : ℝ@i
10. : ℝ@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