---

Step * of Lemma has-minimum-maps-compact

∀I:Interval. ∀l:ℝ. ∀f:I ⟶ℝ.
  ((∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (f[x] = f[y])))
  ⇒ (∀x:{t:ℝ| t ∈ I} . (l < f[x]))
  ⇒ (∀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
{ 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])
⊢ maps-compact(I;(l, ∞);x.f[x])

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 ∈ I ∈ Type)
7. a : ℝ
8. a ∈ I
9. ∀b:ℝ. ((b ∈ I) ∧ (a ≤ b) ∈ Type)
10. b : ℝ
11. b ∈ I
12. a ≤ b
13. ∀t:ℝ. (t ∈ [a, b] ∈ Type)
14. c : ℝ
15. c ∈ [a, b]
16. ∀t:ℝ. (t ∈ [a, b] ∈ Type)
17. x : ℝ
18. x ∈ [a, b]
⊢ c ∈ {x:ℝ| x ∈ I} 

3
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 ∈ I ∈ Type)
7. a : ℝ
8. a ∈ I
9. ∀b:ℝ. ((b ∈ I) ∧ (a ≤ b) ∈ Type)
10. b : ℝ
11. b ∈ I
12. a ≤ b
13. ∀t:ℝ. (t ∈ [a, b] ∈ Type)
14. c : ℝ
15. c ∈ [a, b]
16. ∀t:ℝ. (t ∈ [a, b] ∈ Type)
17. x : ℝ
18. x ∈ [a, b]
⊢ x ∈ {x:ℝ| x ∈ I} 

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}l:\mBbbR{}.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y])))
    {}\mRightarrow{}  (\mforall{}x:\{t:\mBbbR{}|  t  \mmember{}  I\}  .  (l  <  f[x]))
    {}\mRightarrow{}  (\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]))
    {}\mRightarrow{}  maps-compact(I;(l,  \minfty{});x.f[x]))


By

---

Latex:
Auto

---

Home Index