---

Step * of Lemma fun-converges-to-integral

∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ. ∀F:I ⟶ℝ.
  (lim n→∞.f[n;x] = λy.F[y] for x ∈ I
  ⇒ (∀n:ℕ. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (f[n;x] = f[n;y])))
  ⇒ (∀a:{a:ℝ| a ∈ I} . lim n→∞.a_∫-x f[n;t] dt = λx.a_∫-x F[t] dt for x ∈ I))
BY
{ (Auto THEN Assert ⌜∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (F[x] = F[y]))⌝⋅) }

1
.....assertion..... 
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. F : I ⟶ℝ
4. lim n→∞.f[n;x] = λy.F[y] for x ∈ I
5. ∀n:ℕ. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (f[n;x] = f[n;y]))
6. a : {a:ℝ| a ∈ I} 
⊢ ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (F[x] = F[y]))

2
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. F : I ⟶ℝ
4. lim n→∞.f[n;x] = λy.F[y] for x ∈ I
5. ∀n:ℕ. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (f[n;x] = f[n;y]))
6. a : {a:ℝ| a ∈ I} 
7. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (F[x] = F[y]))
⊢ lim n→∞.a_∫-x f[n;t] dt = λx.a_∫-x F[t] dt for x ∈ I

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.  \mforall{}F:I  {}\mrightarrow{}\mBbbR{}.
    (lim  n\mrightarrow{}\minfty{}.f[n;x]  =  \mlambda{}y.F[y]  for  x  \mmember{}  I
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[n;x]  =  f[n;y])))
    {}\mRightarrow{}  (\mforall{}a:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  lim  n\mrightarrow{}\minfty{}.a\_\mint{}\msupminus{}x  f[n;t]  dt  =  \mlambda{}x.a\_\mint{}\msupminus{}x  F[t]  dt  for  x  \mmember{}  I))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (F[x]  =  F[y]))\mkleeneclose{}\mcdot{})

---

Home Index