---

Step * 1 of Lemma Taylor-theorem-for-2


1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (h[x] = h[y]))
7. d(f[x])/dx = λx.g[x] on I
8. d(g[x])/dx = λx.h[x] on I
9. a : {a:ℝ| a ∈ I} 
10. b : {a:ℝ| a ∈ I} 
11. e : ℝ
12. r0 < e
13. k : ℕ1 + 2
14. x : {a:ℝ| a ∈ I} 
15. y : {a:ℝ| a ∈ I} 
16. x = y
⊢ [f[x]; g[x]; h[x]][k] = [f[y]; g[y]; h[y]][k]
BY
{ ((InstLemma `differentiable-functional2` [⌜I⌝;⌜g⌝;⌜h⌝]⋅ THENA Auto)
   THEN (InstLemma `differentiable-functional2` [⌜I⌝;⌜f⌝;⌜g⌝]⋅ THENA Auto)
   ) }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (h[x] = h[y]))
7. d(f[x])/dx = λx.g[x] on I
8. d(g[x])/dx = λx.h[x] on I
9. a : {a:ℝ| a ∈ I} 
10. b : {a:ℝ| a ∈ I} 
11. e : ℝ
12. r0 < e
13. k : ℕ1 + 2
14. x : {a:ℝ| a ∈ I} 
15. y : {a:ℝ| a ∈ I} 
16. x = y
17. ∀a,b:{x:ℝ| x ∈ I} .  ((a = b) ⇒ (g[a] = g[b]))
18. ∀a,b:{x:ℝ| x ∈ I} .  ((a = b) ⇒ (f[a] = f[b]))
⊢ [f[x]; g[x]; h[x]][k] = [f[y]; g[y]; h[y]][k]

---

Latex:

---

Latex:

1.  I  :  Interval
2.  iproper(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  g  :  I  {}\mrightarrow{}\mBbbR{}
5.  h  :  I  {}\mrightarrow{}\mBbbR{}
6.  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (h[x]  =  h[y]))
7.  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
8.  d(g[x])/dx  =  \mlambda{}x.h[x]  on  I
9.  a  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
10.  b  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
11.  e  :  \mBbbR{}
12.  r0  <  e
13.  k  :  \mBbbN{}1  +  2
14.  x  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
15.  y  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
16.  x  =  y
\mvdash{}  [f[x];  g[x];  h[x]][k]  =  [f[y];  g[y];  h[y]][k]


By

---

Latex:
((InstLemma  `differentiable-functional2`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `differentiable-functional2`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index