Step * 1 1 of Lemma second-deriv-implies-nonzero-on


1. Interval
2. iproper(I)
3. I ⟶ℝ
4. I ⟶ℝ
5. 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. ∀x:{a:ℝa ∈ I} (h[x] ≤ r0)
10. ∀x:ℝ((x ∈ I)  (r0 < f[x]))
11. : ℝ
12. : ℝ
13. x ∈ I
14. y ∈ I
15. y
⊢ f[x] f[y]
BY
((InstLemma `differentiable-functional2` [⌜I⌝;⌜g⌝;⌜h⌝]⋅ THENA Auto)
   THEN InstLemma `differentiable-functional2` [⌜I⌝;⌜f⌝;⌜g⌝]⋅
   THEN Auto) }


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.  \mforall{}x:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  (h[x]  \mleq{}  r0)
10.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  I)  {}\mRightarrow{}  (r0  <  f[x]))
11.  x  :  \mBbbR{}
12.  y  :  \mBbbR{}
13.  x  \mmember{}  I
14.  y  \mmember{}  I
15.  x  =  y
\mvdash{}  f[x]  =  f[y]


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{}
  THEN  Auto)




Home Index