---

Step * of Lemma fun-series-converges-on-compact

∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ.
  ((∀m:{m:ℕ+| icompact(i-approx(I;m))} . Σn.f[n;x]↓ for x ∈ i-approx(I;m)) ⇒ Σn.f[n;x]↓ for x ∈ I)
BY
{ (Unfold `fun-series-converges` 0⋅
   THEN EAuto 1
   THEN (Unfold `label` 0 THEN Auto THEN D (-2) THEN FLemma `i-member-approx` [-2] THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}  .  \mSigma{}n.f[n;x]\mdownarrow{}  for  x  \mmember{}  i-approx(I;m))  {}\mRightarrow{}  \mSigma{}n.f[n;x]\mdownarrow{}  for  x  \mmember{}  I)


By

---

Latex:
(Unfold  `fun-series-converges`  0\mcdot{}
  THEN  EAuto  1
  THEN  (Unfold  `label`  0  THEN  Auto  THEN  D  (-2)  THEN  FLemma  `i-member-approx`  [-2]  THEN  Auto)\mcdot{})

---

Home Index