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


1. Interval
2. : ℝ
3. 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])
⊢ maps-compact(I;(l, ∞);x.f[x])
BY
(D THEN Auto) }

1
1. Interval
2. : ℝ
3. 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. {n:ℕ+icompact(i-approx(I;n))} 
⊢ ∃m:{m:ℕ+icompact(i-approx((l, ∞);m))} . ∀x:{x:ℝx ∈ i-approx(I;n)} (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])
\mvdash{}  maps-compact(I;(l,  \minfty{});x.f[x])


By


Latex:
(D  0  THEN  Auto)




Home Index