---

Step * of Lemma differentiable-continuous

∀I:Interval. ∀f,g:I ⟶ℝ.
  ((∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))) ⇒ d(f[x])/dx = λx.g[x] on I ⇒ f[x] (proper)continuous for x ∈ I)
BY
{ xxx(Auto THEN (FLemma `function-proper-continuous` [-2] THENA Auto))xxx }

1
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. d(f[x])/dx = λx.g[x] on I
6. g[x] (proper)continuous for x ∈ I
⊢ f[x] (proper)continuous for x ∈ I

---

Latex:

---

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


By

---

Latex:
xxx(Auto  THEN  (FLemma  `function-proper-continuous`  [-2]  THENA  Auto))xxx

---

Home Index