---

Step * 1 1 1 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. n : ℕ+
8. 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))
BY
{ (((FLemma `icompact-is-rccint` [-1] THENA Auto) THEN HypSubst (-1) 0)
   THEN (Assert i-approx(I;n) ⊆ I  BY
               Auto)
   THEN ((Assert left-endpoint(i-approx(I;n)) ∈ I BY (BackThruHyp' (-1) THEN EAuto 1)) THEN MoveToConcl (-1))
   THEN (Assert right-endpoint(i-approx(I;n)) ∈ I BY
               (BackThruHyp' (-1) THEN EAuto 1))
   THEN MoveToConcl (-1)
   THEN Assert ⌜left-endpoint(i-approx(I;n)) ≤ right-endpoint(i-approx(I;n))⌝⋅) }

1
.....assertion..... 
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. n : ℕ+
8. icompact(i-approx(I;n))
9. i-approx(I;n) ~ [left-endpoint(i-approx(I;n)), right-endpoint(i-approx(I;n))]
10. i-approx(I;n) ⊆ I 
⊢ left-endpoint(i-approx(I;n)) ≤ right-endpoint(i-approx(I;n))

2
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. n : ℕ+
8. icompact(i-approx(I;n))
9. i-approx(I;n) ~ [left-endpoint(i-approx(I;n)), right-endpoint(i-approx(I;n))]
10. i-approx(I;n) ⊆ I 
11. left-endpoint(i-approx(I;n)) ≤ right-endpoint(i-approx(I;n))
⊢ (right-endpoint(i-approx(I;n)) ∈ I)
⇒ (left-endpoint(i-approx(I;n)) ∈ I)
⇒ (∃m:{m:ℕ+| icompact(i-approx((l, ∞);m))} 
     ∀x:{x:ℝ| x ∈ [left-endpoint(i-approx(I;n)), right-endpoint(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])
7.  n  :  \mBbbN{}\msupplus{}
8.  icompact(i-approx(I;n))
\mvdash{}  \mexists{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx((l,  \minfty{});m))\}  .  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;n)\}  .  (f[x]  \mmember{}  i-approx((l,  \minfty{});m)\000C)


By

---

Latex:
(((FLemma  `icompact-is-rccint`  [-1]  THENA  Auto)  THEN  HypSubst  (-1)  0)
  THEN  (Assert  i-approx(I;n)  \msubseteq{}  I    BY
                          Auto)
  THEN  ((Assert  left-endpoint(i-approx(I;n))  \mmember{}  I  BY
                            (BackThruHyp'  (-1)  THEN  EAuto  1))
              THEN  MoveToConcl  (-1)
              )
  THEN  (Assert  right-endpoint(i-approx(I;n))  \mmember{}  I  BY
                          (BackThruHyp'  (-1)  THEN  EAuto  1))
  THEN  MoveToConcl  (-1)
  THEN  Assert  \mkleeneopen{}left-endpoint(i-approx(I;n))  \mleq{}  right-endpoint(i-approx(I;n))\mkleeneclose{}\mcdot{})

---

Home Index