---

Step * of Lemma derivative-implies-decreasing

∀I:Interval
  (iproper(I)
  ⇒ (∀f,f':I ⟶ℝ.
        (d(f[x])/dx = λx.f'[x] on I
        ⇒ f'[x] continuous for x ∈ I
        ⇒ (∀x:{x:ℝ| x ∈ I} . (f'[x] ≤ r0))
        ⇒ f[x] decreasing for x ∈ I)))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (Assert [x, y] ⊆ I  BY
               EAuto 1)
   THEN (InstLemma `continuous_functionality_wrt_subinterval` [⌜I⌝;⌜f'⌝;⌜[x, y]⌝]⋅ THENA Auto)) }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. d(f[x])/dx = λx.f'[x] on I
6. f'[x] continuous for x ∈ I
7. ∀x:{x:ℝ| x ∈ I} . (f'[x] ≤ r0)
8. x : {x:ℝ| x ∈ I} 
9. y : {x:ℝ| x ∈ I} 
10. x ≤ y
11. [x, y] ⊆ I 
12. f'[x] continuous for x ∈ [x, y]
⊢ f[y] ≤ f[x]

---

Latex:

---

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}f,f':I  {}\mrightarrow{}\mBbbR{}.
                (d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
                {}\mRightarrow{}  f'[x]  continuous  for  x  \mmember{}  I
                {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f'[x]  \mleq{}  r0))
                {}\mRightarrow{}  f[x]  decreasing  for  x  \mmember{}  I)))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (Assert  [x,  y]  \msubseteq{}  I    BY
                          EAuto  1)
  THEN  (InstLemma  `continuous\_functionality\_wrt\_subinterval`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}[x,  y]\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index