---

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


1. J : Interval
2. n : ℕ+
3. a : ℝ
4. b : ℝ
5. a ≤ b
6. g : [a, b] ⟶ℝ
7. interval-fun([a, b];J;x.g[x])
8. real-fun(g;a;b)
9. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
10. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
11. bnd : ℝ
12. r0 ≤ bnd
13. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
⊢ ∃m:{m:ℕ+| icompact(i-approx(J;m))} . ∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ i-approx(J;m))
BY
{ Assert ⌜∃c,d:ℝ. ([c, d] ⊆ J  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))⌝⋅ }

1
.....assertion..... 
1. J : Interval
2. n : ℕ+
3. a : ℝ
4. b : ℝ
5. a ≤ b
6. g : [a, b] ⟶ℝ
7. interval-fun([a, b];J;x.g[x])
8. real-fun(g;a;b)
9. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
10. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
11. bnd : ℝ
12. r0 ≤ bnd
13. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
⊢ ∃c,d:ℝ. ([c, d] ⊆ J  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))

2
1. J : Interval
2. n : ℕ+
3. a : ℝ
4. b : ℝ
5. a ≤ b
6. g : [a, b] ⟶ℝ
7. interval-fun([a, b];J;x.g[x])
8. real-fun(g;a;b)
9. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
10. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
11. bnd : ℝ
12. r0 ≤ bnd
13. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
14. ∃c,d:ℝ. ([c, d] ⊆ J  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))
⊢ ∃m:{m:ℕ+| icompact(i-approx(J;m))} . ∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ i-approx(J;m))

---

Latex:

---

Latex:

1.  J  :  Interval
2.  n  :  \mBbbN{}\msupplus{}
3.  a  :  \mBbbR{}
4.  b  :  \mBbbR{}
5.  a  \mleq{}  b
6.  g  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
7.  interval-fun([a,  b];J;x.g[x])
8.  real-fun(g;a;b)
9.  \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))))
10.  \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')))
11.  bnd  :  \mBbbR{}
12.  r0  \mleq{}  bnd
13.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  (|g  x|  \mleq{}  bnd))
\mvdash{}  \mexists{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx(J;m))\}  .  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (g[x]  \mmember{}  i-approx(J;m))


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}c,d:\mBbbR{}.  ([c,  d]  \msubseteq{}  J    \mwedge{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (g[x]  \mmember{}  [c,  d])))\mkleeneclose{}\mcdot{}

---

Home Index