---

Step * of Lemma derivative-continuous

∀I:Interval. ∀f,g:I ⟶ℝ.
  ((∀x,y:{x:ℝ| x ∈ I} .  (g[x] ≠ g[y] ⇒ x ≠ y)) ⇒ λx.g[x] = d(f[x])/dx on I ⇒ g[x] continuous for x ∈ I)
BY
{ (Auto THEN D 0 THEN Auto) }

1
1. I : Interval@i
2. f : I ⟶ℝ@i
3. g : I ⟶ℝ@i
4. ∀x,y:{x:ℝ| x ∈ I} .  (g[x] ≠ g[y] ⇒ x ≠ y)@i
5. λx.g[x] = d(f[x])/dx on I@i
6. m : {m:ℕ+| icompact(i-approx(I;m))} @i
7. n : ℕ+@i
⊢ ∃d:{ℝ| ((r0 < d)
         ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))))}

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f,g:I  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (g[x]  \mneq{}  g[y]  {}\mRightarrow{}  x  \mneq{}  y))
    {}\mRightarrow{}  \mlambda{}x.g[x]  =  d(f[x])/dx  on  I
    {}\mRightarrow{}  g[x]  continuous  for  x  \mmember{}  I)


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index