---

Step * 1 1 1 of Lemma fun-converges-to-integral


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 : ℝ
7. a ∈ I
8. ∀x:ℝ. ((x ∈ I) ⇒ lim n→∞.f[n;x] = F[x])
9. x : ℝ
10. x ∈ I
11. y : ℝ
12. y ∈ I
13. x = y
14. lim n→∞.f[n;x] = F[x] ∧ lim n→∞.f[n;y] = F[y]
⊢ F[x] = F[y]
BY
{ (D -1 THEN Assert ⌜lim n→∞.f[n;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 : ℝ
7. a ∈ I
8. ∀x:ℝ. ((x ∈ I) ⇒ lim n→∞.f[n;x] = F[x])
9. x : ℝ
10. x ∈ I
11. y : ℝ
12. y ∈ I
13. x = y
14. lim n→∞.f[n;x] = F[x]
15. lim n→∞.f[n;y] = F[y]
⊢ lim n→∞.f[n;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 : ℝ
7. a ∈ I
8. ∀x:ℝ. ((x ∈ I) ⇒ lim n→∞.f[n;x] = F[x])
9. x : ℝ
10. x ∈ I
11. y : ℝ
12. y ∈ I
13. x = y
14. lim n→∞.f[n;x] = F[x]
15. lim n→∞.f[n;y] = F[y]
16. lim n→∞.f[n;x] = F[y]
⊢ F[x] = F[y]

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  \mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}
3.  F  :  I  {}\mrightarrow{}\mBbbR{}
4.  lim  n\mrightarrow{}\minfty{}.f[n;x]  =  \mlambda{}y.F[y]  for  x  \mmember{}  I
5.  \mforall{}n:\mBbbN{}.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[n;x]  =  f[n;y]))
6.  a  :  \mBbbR{}
7.  a  \mmember{}  I
8.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  I)  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.f[n;x]  =  F[x])
9.  x  :  \mBbbR{}
10.  x  \mmember{}  I
11.  y  :  \mBbbR{}
12.  y  \mmember{}  I
13.  x  =  y
14.  lim  n\mrightarrow{}\minfty{}.f[n;x]  =  F[x]  \mwedge{}  lim  n\mrightarrow{}\minfty{}.f[n;y]  =  F[y]
\mvdash{}  F[x]  =  F[y]


By

---

Latex:
(D  -1  THEN  Assert  \mkleeneopen{}lim  n\mrightarrow{}\minfty{}.f[n;x]  =  F[y]\mkleeneclose{}\mcdot{})

---

Home Index