---

Step * 2 of Lemma derivative-mul


1. I : Interval
2. f1 : I ⟶ℝ
3. f2 : I ⟶ℝ
4. g1 : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
5. g2 : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
6. d(f1 x)/dx = λx.g1 x on I
7. d(f2 x)/dx = λx.g2 x on I
⊢ λ2x.f2 x(x) (proper)continuous for x ∈ I
BY
{ ((FLemma `differentiable-continuous` [-1] THEN Auto) THEN DVar `g2' THEN Unhide THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f1  :  I  {}\mrightarrow{}\mBbbR{}
3.  f2  :  I  {}\mrightarrow{}\mBbbR{}
4.  g1  :  \{h:I  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((h  x)  =  (h  y)))\} 
5.  g2  :  \{h:I  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((h  x)  =  (h  y)))\} 
6.  d(f1  x)/dx  =  \mlambda{}x.g1  x  on  I
7.  d(f2  x)/dx  =  \mlambda{}x.g2  x  on  I
\mvdash{}  \mlambda{}\msubtwo{}x.f2  x(x)  (proper)continuous  for  x  \mmember{}  I


By

---

Latex:
((FLemma  `differentiable-continuous`  [-1]  THEN  Auto)  THEN  DVar  `g2'  THEN  Unhide  THEN  Auto)

---

Home Index