---

Step * of Lemma IVT-strictly-increasing-open

∀a:ℝ. ∀b:{b:ℝ| a < b} . ∀f:[a, b] ⟶ℝ.
  f[x] strictly-increasing for x ∈ (a, b) ⇒ (∀c:ℝ. ((f(a) < c) ⇒ (c < f(b)) ⇒ (∃x:ℝ. ((x ∈ (a, b)) ∧ (f(x) = c))))) 
  supposing ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (f[x] = f[y]))
BY
{ (InstLemma `IVT-locally-non-constant-open` []
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN (Assert (a, b) ⊆ [a, b]  BY
               (D 0 THEN Reduce 0 THEN Auto))
   THEN ParallelOp -2
   THEN Auto) }

1
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (f[x] = f[y]))
5. (a, b) ⊆ [a, b] 
6. f[x] strictly-increasing for x ∈ (a, b)
7. a' : ℝ
8. b' : ℝ
9. a < a'
10. a' < b'
11. b' < b
12. c : ℝ
⊢ locally-non-constant(f;a';b';c)

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  <  b\}  .  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.
    f[x]  strictly-increasing  for  x  \mmember{}  (a,  b)
    {}\mRightarrow{}  (\mforall{}c:\mBbbR{}.  ((f(a)  <  c)  {}\mRightarrow{}  (c  <  f(b))  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  ((x  \mmember{}  (a,  b))  \mwedge{}  (f(x)  =  c))))) 
    supposing  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))


By

---

Latex:
(InstLemma  `IVT-locally-non-constant-open`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  (Assert  (a,  b)  \msubseteq{}  [a,  b]    BY
                          (D  0  THEN  Reduce  0  THEN  Auto))
  THEN  ParallelOp  -2
  THEN  Auto)

---

Home Index