---

Step * 1 of Lemma continuous-mul

.....assertion..... 
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. rmax(|f[x]|;|g[x]|) continuous for x ∈ I
5. m : {m:ℕ+| icompact(i-approx(I;m))} 
6. n : ℕ+
7. ∀n:ℕ+
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))})
8. ∀n:ℕ+
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))))})
⊢ ∃N:ℕ+. ∀[x:{r:ℝ| r ∈ i-approx(I;m)} ]. (rmax(|f[x]|;|g[x]|) ≤ r(N))
BY
{ ((InstLemma `continuous_functionality_wrt_subinterval` [⌜I⌝;⌜λ2x.rmax(|f[x]|;|g[x]|)⌝;⌜i-approx(I;m)⌝]⋅ THENA Auto)⋅
   THEN RenameVar `mc' (-1)
   THEN (Assert f ∈ i-approx(I;m) ⟶ℝ BY
               Auto)
   THEN (Assert g ∈ i-approx(I;m) ⟶ℝ BY
               Auto)
   THEN (InstLemma `Inorm-bound` [⌜i-approx(I;m)⌝;⌜λ2x.rmax(|f[x]|;|g[x]|)⌝;⌜mc⌝]⋅ THENA Auto)
   THEN With ⌜r-bound(||rmax(|f[x]|;|g[x]|)||_i-approx(I;m))⌝ (D 0)⋅
   THEN Auto
   THEN (Assert |rmax(|f[x]|;|g[x]|)| ≤ r(r-bound(||rmax(|f[x]|;|g[x]|)||_i-approx(I;m))) BY
               (RWO  "-2" 0 THEN Auto))
   THEN RWO "-1<" 0
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  g  :  I  {}\mrightarrow{}\mBbbR{}
4.  rmax(|f[x]|;|g[x]|)  continuous  for  x  \mmember{}  I
5.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\} 
6.  n  :  \mBbbN{}\msupplus{}
7.  \mforall{}n:\mBbbN{}\msupplus{}
          (\mexists{}d:\{\mBbbR{}|  ((r0  <  d)
                          \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                    ((x  \mmember{}  i-approx(I;m))
                                    {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
                                    {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
                                    {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(n))))))\})
8.  \mforall{}n:\mBbbN{}\msupplus{}
          (\mexists{}d:\{\mBbbR{}|  ((r0  <  d)
                          \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                    ((x  \mmember{}  i-approx(I;m))
                                    {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
                                    {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
                                    {}\mRightarrow{}  (|g[x]  -  g[y]|  \mleq{}  (r1/r(n))))))\})
\mvdash{}  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;m)\}  ].  (rmax(|f[x]|;|g[x]|)  \mleq{}  r(N))


By

---

Latex:
((InstLemma  `continuous\_functionality\_wrt\_subinterval`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rmax(|f[x]|;|g[x]|)\mkleeneclose{};
    \mkleeneopen{}i-approx(I;m)\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )\mcdot{}
  THEN  RenameVar  `mc'  (-1)
  THEN  (Assert  f  \mmember{}  i-approx(I;m)  {}\mrightarrow{}\mBbbR{}  BY
                          Auto)
  THEN  (Assert  g  \mmember{}  i-approx(I;m)  {}\mrightarrow{}\mBbbR{}  BY
                          Auto)
  THEN  (InstLemma  `Inorm-bound`  [\mkleeneopen{}i-approx(I;m)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rmax(|f[x]|;|g[x]|)\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  With  \mkleeneopen{}r-bound(||rmax(|f[x]|;|g[x]|)||\_i-approx(I;m))\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (Assert  |rmax(|f[x]|;|g[x]|)|  \mleq{}  r(r-bound(||rmax(|f[x]|;|g[x]|)||\_i-approx(I;m)))  BY
                          (RWO    "-2"  0  THEN  Auto))
  THEN  RWO  "-1<"  0
  THEN  Auto)

---

Home Index