---

Step * of Lemma IVT-from-connected

∀u,v:ℝ. ∀f:[u, v] ⟶ℝ.
  ((u ≤ v)
  ⇒ (∀x,y:{x:ℝ| x ∈ [u, v]} .  ((x = y) ⇒ (f(x) = f(y))))
  ⇒ (f(u) < r0)
  ⇒ (r0 < f(v))
  ⇒ (∀e:{e:ℝ| r0 < e} . ∃c:{c:ℝ| c ∈ [u, v]} . (|f(c)| < e)))
BY
{ (InstLemma `closed-interval-connected` []
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto
   THEN Unfold `connected` 5
   THEN (InstHyp [⌜λ2c.f(c) < e⌝;⌜λ2c.-(e) < f(c)⌝] 5⋅
         THENA (Try (Complete (Auto))
                THEN Try (Complete ((Auto
                                     THEN ((DVar `y' THEN Unhide) THEN Auto)
                                     THEN (Assert f(x) = f(y) BY
                                                 Auto)
                                     THEN Auto)))
                )
         )) }

1
.....antecedent..... 
1. ∀u,v:ℝ.  Connected({x:ℝ| x ∈ [u, v]} )
2. u : ℝ
3. ∀v:ℝ. Connected({x:ℝ| x ∈ [u, v]} )
4. v : ℝ
5. ∀[A,B:{x:ℝ| x ∈ [u, v]}  ⟶ ℙ].
     ((∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (A[y] ⇒ A[x]))
     ⇒ (∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (B[y] ⇒ B[x]))
     ⇒ (∃a:{x:ℝ| x ∈ [u, v]} . A[a])
     ⇒ (∃b:{x:ℝ| x ∈ [u, v]} . B[b])
     ⇒ (∀r:{x:ℝ| x ∈ [u, v]} . (A[r] ∨ B[r]))
     ⇒ (∃r:{x:ℝ| x ∈ [u, v]} . (A[r] ∧ B[r])))
6. f : [u, v] ⟶ℝ
7. u ≤ v
8. ∀x,y:{x:ℝ| x ∈ [u, v]} .  ((x = y) ⇒ (f(x) = f(y)))
9. f(u) < r0
10. r0 < f(v)
11. e : {e:ℝ| r0 < e} 
⊢ ∃a:{x:ℝ| x ∈ [u, v]} . (f(a) < e)

2
.....antecedent..... 
1. ∀u,v:ℝ.  Connected({x:ℝ| x ∈ [u, v]} )
2. u : ℝ
3. ∀v:ℝ. Connected({x:ℝ| x ∈ [u, v]} )
4. v : ℝ
5. ∀[A,B:{x:ℝ| x ∈ [u, v]}  ⟶ ℙ].
     ((∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (A[y] ⇒ A[x]))
     ⇒ (∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (B[y] ⇒ B[x]))
     ⇒ (∃a:{x:ℝ| x ∈ [u, v]} . A[a])
     ⇒ (∃b:{x:ℝ| x ∈ [u, v]} . B[b])
     ⇒ (∀r:{x:ℝ| x ∈ [u, v]} . (A[r] ∨ B[r]))
     ⇒ (∃r:{x:ℝ| x ∈ [u, v]} . (A[r] ∧ B[r])))
6. f : [u, v] ⟶ℝ
7. u ≤ v
8. ∀x,y:{x:ℝ| x ∈ [u, v]} .  ((x = y) ⇒ (f(x) = f(y)))
9. f(u) < r0
10. r0 < f(v)
11. e : {e:ℝ| r0 < e} 
⊢ ∃b:{x:ℝ| x ∈ [u, v]} . (-(e) < f(b))

3
.....antecedent..... 
1. ∀u,v:ℝ.  Connected({x:ℝ| x ∈ [u, v]} )
2. u : ℝ
3. ∀v:ℝ. Connected({x:ℝ| x ∈ [u, v]} )
4. v : ℝ
5. ∀[A,B:{x:ℝ| x ∈ [u, v]}  ⟶ ℙ].
     ((∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (A[y] ⇒ A[x]))
     ⇒ (∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (B[y] ⇒ B[x]))
     ⇒ (∃a:{x:ℝ| x ∈ [u, v]} . A[a])
     ⇒ (∃b:{x:ℝ| x ∈ [u, v]} . B[b])
     ⇒ (∀r:{x:ℝ| x ∈ [u, v]} . (A[r] ∨ B[r]))
     ⇒ (∃r:{x:ℝ| x ∈ [u, v]} . (A[r] ∧ B[r])))
6. f : [u, v] ⟶ℝ
7. u ≤ v
8. ∀x,y:{x:ℝ| x ∈ [u, v]} .  ((x = y) ⇒ (f(x) = f(y)))
9. f(u) < r0
10. r0 < f(v)
11. e : {e:ℝ| r0 < e} 
⊢ ∀r:{x:ℝ| x ∈ [u, v]} . ((f(r) < e) ∨ (-(e) < f(r)))

4
1. ∀u,v:ℝ.  Connected({x:ℝ| x ∈ [u, v]} )
2. u : ℝ
3. ∀v:ℝ. Connected({x:ℝ| x ∈ [u, v]} )
4. v : ℝ
5. ∀[A,B:{x:ℝ| x ∈ [u, v]}  ⟶ ℙ].
     ((∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (A[y] ⇒ A[x]))
     ⇒ (∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (B[y] ⇒ B[x]))
     ⇒ (∃a:{x:ℝ| x ∈ [u, v]} . A[a])
     ⇒ (∃b:{x:ℝ| x ∈ [u, v]} . B[b])
     ⇒ (∀r:{x:ℝ| x ∈ [u, v]} . (A[r] ∨ B[r]))
     ⇒ (∃r:{x:ℝ| x ∈ [u, v]} . (A[r] ∧ B[r])))
6. f : [u, v] ⟶ℝ
7. u ≤ v
8. ∀x,y:{x:ℝ| x ∈ [u, v]} .  ((x = y) ⇒ (f(x) = f(y)))
9. f(u) < r0
10. r0 < f(v)
11. e : {e:ℝ| r0 < e} 
12. ∃r:{x:ℝ| x ∈ [u, v]} . ((f(r) < e) ∧ (-(e) < f(r)))
⊢ ∃c:{c:ℝ| c ∈ [u, v]} . (|f(c)| < e)

---

Latex:

---

Latex:
\mforall{}u,v:\mBbbR{}.  \mforall{}f:[u,  v]  {}\mrightarrow{}\mBbbR{}.
    ((u  \mleq{}  v)
    {}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))
    {}\mRightarrow{}  (f(u)  <  r0)
    {}\mRightarrow{}  (r0  <  f(v))
    {}\mRightarrow{}  (\mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .  \mexists{}c:\{c:\mBbbR{}|  c  \mmember{}  [u,  v]\}  .  (|f(c)|  <  e)))


By

---

Latex:
(InstLemma  `closed-interval-connected`  []
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto
  THEN  Unfold  `connected`  5
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}c.f(c)  <  e\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}c.-(e)  <  f(c)\mkleeneclose{}]  5\mcdot{}
              THENA  (Try  (Complete  (Auto))
                            THEN  Try  (Complete  ((Auto
                                                                      THEN  ((DVar  `y'  THEN  Unhide)  THEN  Auto)
                                                                      THEN  (Assert  f(x)  =  f(y)  BY
                                                                                              Auto)
                                                                      THEN  Auto)))
                            )
              ))

---

Home Index