---

Step * of Lemma fun-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
{ (Auto
   THEN Try ((Unfold `label` 0 THEN Auto THEN D (-1) THEN FLemma `i-member-approx` [-1] THEN Auto))
   THEN BLemma `fun-converges-iff-cauchy`
   THEN Auto
   THEN Unfold `fun-cauchy` 0
   THEN ParallelLast
   THEN (Assert i-approx(I;a) ⊆ I  BY
               Auto)
   THEN (RWO "fun-converges-iff-cauchy" (-2) THENA Auto)) }

1
1. I : Interval@i
2. f : ℕ ⟶ I ⟶ℝ@i
3. ∀m:{m:ℕ+| icompact(i-approx(I;m))} . λn.f[n;x]↓ for x ∈ i-approx(I;m))@i
4. a : {a:ℕ+| icompact(i-approx(I;a))} @i
5. λn.f[n;x] is cauchy for x ∈ i-approx(I;a)
6. i-approx(I;a) ⊆ I 
⊢ ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . ∀n,m:{N...}.  (|f[n;x] - f[m;x]| ≤ (r1/r(k)))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Try  ((Unfold  `label`  0  THEN  Auto  THEN  D  (-1)  THEN  FLemma  `i-member-approx`  [-1]  THEN  Auto))
  THEN  BLemma  `fun-converges-iff-cauchy`
  THEN  Auto
  THEN  Unfold  `fun-cauchy`  0
  THEN  ParallelLast
  THEN  (Assert  i-approx(I;a)  \msubseteq{}  I    BY
                          Auto)
  THEN  (RWO  "fun-converges-iff-cauchy"  (-2)  THENA  Auto))

---

Home Index