---

Step * of Lemma fun-converges-to-derivative

∀I:Interval
  (iproper(I)
  ⇒ (∀f,f':ℕ ⟶ I ⟶ℝ. ∀F,G:I ⟶ℝ.
        ((∀n:ℕ. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (f'[n;x] = f'[n;y])))
        ⇒ lim n→∞.f[n;x] = λy.F[y] for x ∈ I
        ⇒ lim n→∞.f'[n;x] = λy.G[y] for x ∈ I
        ⇒ (∀n:ℕ. d(f[n;x])/dx = λx.f'[n;x] on I)
        ⇒ d(F[x])/dx = λx.G[x] on I)))
BY
{ TACTIC:((Auto THEN (FLemma `iproper-nonvoid` [2] THENA Auto) THEN D -1)
          THEN Assert ⌜∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (G[x] = G[y]))⌝⋅
          ) }

1
.....assertion..... 
1. I : Interval
2. iproper(I)
3. f : ℕ ⟶ I ⟶ℝ
4. f' : ℕ ⟶ I ⟶ℝ
5. F : I ⟶ℝ
6. G : I ⟶ℝ
7. ∀n:ℕ. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (f'[n;x] = f'[n;y]))
8. lim n→∞.f[n;x] = λy.F[y] for x ∈ I
9. lim n→∞.f'[n;x] = λy.G[y] for x ∈ I
10. ∀n:ℕ. d(f[n;x])/dx = λx.f'[n;x] on I
11. r : ℝ
12. r ∈ I
⊢ ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (G[x] = G[y]))

2
1. I : Interval
2. iproper(I)
3. f : ℕ ⟶ I ⟶ℝ
4. f' : ℕ ⟶ I ⟶ℝ
5. F : I ⟶ℝ
6. G : I ⟶ℝ
7. ∀n:ℕ. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (f'[n;x] = f'[n;y]))
8. lim n→∞.f[n;x] = λy.F[y] for x ∈ I
9. lim n→∞.f'[n;x] = λy.G[y] for x ∈ I
10. ∀n:ℕ. d(f[n;x])/dx = λx.f'[n;x] on I
11. r : ℝ
12. r ∈ I
13. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (G[x] = G[y]))
⊢ d(F[x])/dx = λx.G[x] on I

---

Latex:

---

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}f,f':\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.  \mforall{}F,G:I  {}\mrightarrow{}\mBbbR{}.
                ((\mforall{}n:\mBbbN{}.  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[n;x]  =  f'[n;y])))
                {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.f[n;x]  =  \mlambda{}y.F[y]  for  x  \mmember{}  I
                {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.f'[n;x]  =  \mlambda{}y.G[y]  for  x  \mmember{}  I
                {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  d(f[n;x])/dx  =  \mlambda{}x.f'[n;x]  on  I)
                {}\mRightarrow{}  d(F[x])/dx  =  \mlambda{}x.G[x]  on  I)))


By

---

Latex:
TACTIC:((Auto  THEN  (FLemma  `iproper-nonvoid`  [2]  THENA  Auto)  THEN  D  -1)
                THEN  Assert  \mkleeneopen{}\mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (G[x]  =  G[y]))\mkleeneclose{}\mcdot{}
                )

---

Home Index