---

Step * of Lemma intermediate-value-theorem

No Annotations
∀I:Interval. ∀f:I ⟶ℝ.
  (f[x] continuous for x ∈ I
  ⇒ (∀a,b:{x:ℝ| x ∈ I} .
        ((f(a) < f(b))
        ⇒ (∀y:{y:ℝ| y ∈ [f(a), f(b)]} . ∀e:{e:ℝ| r0 < e} .  ∃x:{x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} . (|f(x) - y| < e)))))
BY
{ (Auto
   THEN (Assert ⌜a ≠ b⌝ BY
               ((InstLemma `continuous-rneq` [⌜I⌝;⌜f⌝;⌜a⌝;⌜b⌝]⋅
                 THENA (Auto THEN Unfold `so_apply` 0 THEN Fold `r-ap` 0)
                 )
                THEN Auto
                ))
   THEN D -1) }

1
1. I : Interval
2. f : I ⟶ℝ
3. f[x] continuous for x ∈ I
4. a : {x:ℝ| x ∈ I} 
5. b : {x:ℝ| x ∈ I} 
6. f(a) < f(b)
7. y : {y:ℝ| y ∈ [f(a), f(b)]} 
8. e : {e:ℝ| r0 < e} 
9. a < b
⊢ ∃x:{x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} . (|f(x) - y| < e)

2
1. I : Interval
2. f : I ⟶ℝ
3. f[x] continuous for x ∈ I
4. a : {x:ℝ| x ∈ I} 
5. b : {x:ℝ| x ∈ I} 
6. f(a) < f(b)
7. y : {y:ℝ| y ∈ [f(a), f(b)]} 
8. e : {e:ℝ| r0 < e} 
9. b < a
⊢ ∃x:{x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} . (|f(x) - y| < e)

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    (f[x]  continuous  for  x  \mmember{}  I
    {}\mRightarrow{}  (\mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  I\}  .
                ((f(a)  <  f(b))
                {}\mRightarrow{}  (\mforall{}y:\{y:\mBbbR{}|  y  \mmember{}  [f(a),  f(b)]\}  .  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
                            \mexists{}x:\{x:\mBbbR{}|  x  \mmember{}  [rmin(a;b),  rmax(a;b)]\}  .  (|f(x)  -  y|  <  e)))))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}a  \mneq{}  b\mkleeneclose{}  BY
                          ((InstLemma  `continuous-rneq`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
                              THENA  (Auto  THEN  Unfold  `so\_apply`  0  THEN  Fold  `r-ap`  0)
                              )
                            THEN  Auto
                            ))
  THEN  D  -1)

---

Home Index