---

Step * 1 1 1 5 of Lemma interval-fun-maps-compact


1. y : Top
2. x1 : ℝ
3. n : ℕ+
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ <inr y , inl inl x1>)
9. ∀x,y:{x:ℝ| x ∈ [a, b]} .  g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
⊢ ∃c,d:ℝ. ([c, d] ⊆ <inr y , inl inl x1>  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))
BY
{ ((D 0 With ⌜-(bnd)⌝  THENA Auto) THEN D 0 With ⌜x1⌝  THEN Auto) }

1
1. y : Top
2. x1 : ℝ
3. n : ℕ+
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ <inr y , inl inl x1>)
9. ∀x,y:{x:ℝ| x ∈ [a, b]} .  g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
⊢ [-(bnd), x1] ⊆ <inr y , inl inl x1> 

2
1. y : Top
2. x1 : ℝ
3. n : ℕ+
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ <inr y , inl inl x1>)
9. ∀x,y:{x:ℝ| x ∈ [a, b]} .  g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
16. [-(bnd), x1] ⊆ <inr y , inl inl x1> 
17. x : {x:ℝ| x ∈ [a, b]} 
⊢ g[x] ∈ [-(bnd), x1]

---

Latex:

---

Latex:

1.  y  :  Top
2.  x1  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}
4.  a  :  \mBbbR{}
5.  b  :  \mBbbR{}
6.  a  \mleq{}  b
7.  g  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
8.  \mforall{}x@0:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (g[x@0]  \mmember{}  <inr  y  ,  inl  inl  x1>)
9.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    g[x]  =  g[y]  supposing  x  =  y
10.  real-fun(g;a;b)
11.  \mforall{}c:\mBbbR{}
            ((\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (c  <  (g  x)))
            {}\mRightarrow{}  (\mexists{}c':\{c':\mBbbR{}|  c  <  c'\}  .  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (c'  \mleq{}  (g  x))))
12.  \mforall{}c:\mBbbR{}
            ((\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  ((g  x)  <  c))
            {}\mRightarrow{}  (\mexists{}c':\{c':\mBbbR{}|  c'  <  c\}  .  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  ((g  x)  \mleq{}  c')))
13.  bnd  :  \mBbbR{}
14.  r0  \mleq{}  bnd
15.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  (|g  x|  \mleq{}  bnd))
\mvdash{}  \mexists{}c,d:\mBbbR{}.  ([c,  d]  \msubseteq{}  <inr  y  ,  inl  inl  x1>    \mwedge{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (g[x]  \mmember{}  [c,  d])))


By

---

Latex:
((D  0  With  \mkleeneopen{}-(bnd)\mkleeneclose{}    THENA  Auto)  THEN  D  0  With  \mkleeneopen{}x1\mkleeneclose{}    THEN  Auto)

---

Home Index