---

Step * 3 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.g2 x(x) (proper)continuous for x ∈ I
BY
{ (BLemma `function-proper-continuous`
   THEN RepUR ``so_lambda r-ap`` 0
   THEN Try ((DVar `g2' THEN (Unhide THENM Trivial)))
   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.g2  x(x)  (proper)continuous  for  x  \mmember{}  I


By

---

Latex:
(BLemma  `function-proper-continuous`
  THEN  RepUR  ``so\_lambda  r-ap``  0
  THEN  Try  ((DVar  `g2'  THEN  (Unhide  THENM  Trivial)))
  THEN  Auto)

---

Home Index