---

Step * 1 1 1 2 1 1 1 2 of Lemma has-minimum-maps-compact


1. I : Interval
2. l : ℝ
3. f : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
5. ∀x:{t:ℝ| t ∈ I} . (l < f[x])
6. ∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a ≤ b)} .  ∃c:{t:ℝ| t ∈ [a, b]} . ∀x:{t:ℝ| t ∈ [a, b]} . (f[c] ≤ f[x])
7. a : ℝ
8. b : ℝ
9. [a, b] ⊆ I 
10. a ≤ b
11. b ∈ I
12. a ∈ I
13. c : {t:ℝ| t ∈ [a, b]} 
14. ∀x:{t:ℝ| t ∈ [a, b]} . (f[c] ≤ f[x])
15. f[c] ∈ (l, ∞)
16. sup{f[x] | x ∈ [a, b]} ∈ (l, ∞)
⊢ ∃m:{m:ℕ+| icompact(i-approx((l, ∞);m))} . ∀x:{x:ℝ| x ∈ [a, b]} . (f[x] ∈ i-approx((l, ∞);m))
BY
{ (InstLemma `i-approx-containing2` [⌜(l, ∞)⌝;⌜f[c]⌝;⌜sup{f[x] | x ∈ [a, b]}⌝]⋅ THENA Auto) }

1
1. I : Interval
2. l : ℝ
3. f : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
5. ∀x:{t:ℝ| t ∈ I} . (l < f[x])
6. ∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a ≤ b)} .  ∃c:{t:ℝ| t ∈ [a, b]} . ∀x:{t:ℝ| t ∈ [a, b]} . (f[c] ≤ f[x])
7. a : ℝ
8. b : ℝ
9. [a, b] ⊆ I 
10. a ≤ b
11. b ∈ I
12. a ∈ I
13. c : {t:ℝ| t ∈ [a, b]} 
14. ∀x:{t:ℝ| t ∈ [a, b]} . (f[c] ≤ f[x])
15. f[c] ∈ (l, ∞)
16. sup{f[x] | x ∈ [a, b]} ∈ (l, ∞)
17. ∃n:ℕ+. ((f[c] ∈ i-approx((l, ∞);n)) ∧ (sup{f[x] | x ∈ [a, b]} ∈ i-approx((l, ∞);n)))
⊢ ∃m:{m:ℕ+| icompact(i-approx((l, ∞);m))} . ∀x:{x:ℝ| x ∈ [a, b]} . (f[x] ∈ i-approx((l, ∞);m))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  l  :  \mBbbR{}
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
5.  \mforall{}x:\{t:\mBbbR{}|  t  \mmember{}  I\}  .  (l  <  f[x])
6.  \mforall{}a:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  \mforall{}b:\{b:\mBbbR{}|  (b  \mmember{}  I)  \mwedge{}  (a  \mleq{}  b)\}  .
          \mexists{}c:\{t:\mBbbR{}|  t  \mmember{}  [a,  b]\}  .  \mforall{}x:\{t:\mBbbR{}|  t  \mmember{}  [a,  b]\}  .  (f[c]  \mleq{}  f[x])
7.  a  :  \mBbbR{}
8.  b  :  \mBbbR{}
9.  [a,  b]  \msubseteq{}  I 
10.  a  \mleq{}  b
11.  b  \mmember{}  I
12.  a  \mmember{}  I
13.  c  :  \{t:\mBbbR{}|  t  \mmember{}  [a,  b]\} 
14.  \mforall{}x:\{t:\mBbbR{}|  t  \mmember{}  [a,  b]\}  .  (f[c]  \mleq{}  f[x])
15.  f[c]  \mmember{}  (l,  \minfty{})
16.  sup\{f[x]  |  x  \mmember{}  [a,  b]\}  \mmember{}  (l,  \minfty{})
\mvdash{}  \mexists{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx((l,  \minfty{});m))\}  .  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (f[x]  \mmember{}  i-approx((l,  \minfty{});m))


By

---

Latex:
(InstLemma  `i-approx-containing2`  [\mkleeneopen{}(l,  \minfty{})\mkleeneclose{};\mkleeneopen{}f[c]\mkleeneclose{};\mkleeneopen{}sup\{f[x]  |  x  \mmember{}  [a,  b]\}\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index