---

Step * of Lemma fun-converges-rmul

∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ.
  (λn.f[n;x]↓ for x ∈ I) ⇒ (∀g:I ⟶ℝ. (g[x] continuous for x ∈ I ⇒ λn.f[n;x] * g[x]↓ for x ∈ I))))
BY
{ (Auto
   THEN (RWO "fun-converges-iff-cauchy" (-3) THENA Auto)
   THEN (BLemma `fun-converges-iff-cauchy` THENA Auto)
   THEN RepeatFor 2 (ParallelOp -3)
   THEN Thin 3
   THEN Auto
   THEN Assert ⌜∃M:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . (|g[x]| ≤ r(M))⌝⋅) }

1
.....assertion..... 
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. g : I ⟶ℝ
4. g[x] continuous for x ∈ I
5. a : {a:ℕ+| icompact(i-approx(I;a))} 
6. ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . ∀n,m:{N...}.  (|f[n;x] - f[m;x]| ≤ (r1/r(k)))
7. k : ℕ+
⊢ ∃M:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . (|g[x]| ≤ r(M))

2
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. g : I ⟶ℝ
4. g[x] continuous for x ∈ I
5. a : {a:ℕ+| icompact(i-approx(I;a))} 
6. ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . ∀n,m:{N...}.  (|f[n;x] - f[m;x]| ≤ (r1/r(k)))
7. k : ℕ+
8. ∃M:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . (|g[x]| ≤ r(M))
⊢ ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . ∀n,m:{N...}.  (|(f[n;x] * g[x]) - f[m;x] * g[x]| ≤ (r1/r(k)))

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.
    (\mlambda{}n.f[n;x]\mdownarrow{}  for  x  \mmember{}  I)  {}\mRightarrow{}  (\mforall{}g:I  {}\mrightarrow{}\mBbbR{}.  (g[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  \mlambda{}n.f[n;x]  *  g[x]\mdownarrow{}  for  x  \mmember{}  I))))


By

---

Latex:
(Auto
  THEN  (RWO  "fun-converges-iff-cauchy"  (-3)  THENA  Auto)
  THEN  (BLemma  `fun-converges-iff-cauchy`  THENA  Auto)
  THEN  RepeatFor  2  (ParallelOp  -3)
  THEN  Thin  3
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\mexists{}M:\mBbbN{}\msupplus{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;a)\}  .  (|g[x]|  \mleq{}  r(M))\mkleeneclose{}\mcdot{})

---

Home Index