---

Step * of Lemma fun-converges_functionality

∀[I:Interval]. ∀f,g:ℕ ⟶ I ⟶ℝ.  ((∀n:ℕ. rfun-eq(I;f n;g n)) ⇒ λn.f[n;x]↓ for x ∈ I) ⇒ λn.g[n;x]↓ for x ∈ I))
BY
{ (Auto
   THEN RepeatFor 6 (ParallelLast)
   THEN Try ((DSetVars THEN FLemma `i-member-approx` [-2] THEN Auto))
   THEN RepeatFor 2 (ParallelLast)⋅
   THEN (With ⌜n⌝ (D 4)⋅ THENA Auto)) }

1
1. [I] : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. g : ℕ ⟶ I ⟶ℝ
4. g1 : I ⟶ℝ
5. ∀m:{m:ℕ+| icompact(i-approx(I;m))} . ∀k:ℕ+.
     ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . ∀n:{N...}.  (|f[n;x] - g1 x| ≤ (r1/r(k)))
6. m : {m:ℕ+| icompact(i-approx(I;m))} 
7. ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . ∀n:{N...}.  (|f[n;x] - g1 x| ≤ (r1/r(k)))
8. k : ℕ+
9. N : ℕ+
10. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . ∀n:{N...}.  (|f[n;x] - g1 x| ≤ (r1/r(k)))
11. x : {x:ℝ| x ∈ i-approx(I;m)} 
12. ∀n:{N...}. (|f[n;x] - g1 x| ≤ (r1/r(k)))
13. n : {N...}
14. |f[n;x] - g1 x| ≤ (r1/r(k))
15. rfun-eq(I;f n;g n)
⊢ |g[n;x] - g1 x| ≤ (r1/r(k))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepeatFor  6  (ParallelLast)
  THEN  Try  ((DSetVars  THEN  FLemma  `i-member-approx`  [-2]  THEN  Auto))
  THEN  RepeatFor  2  (ParallelLast)\mcdot{}
  THEN  (With  \mkleeneopen{}n\mkleeneclose{}  (D  4)\mcdot{}  THENA  Auto))

---

Home Index