---

Step * 1 of Lemma inf-range


1. I : {I:Interval| icompact(I)} @i
2. f : I ⟶ℝ@i
3. f(x) continuous for x ∈ I@i
4. totally-bounded(f(x)(x∈I))
5. icompact(I)
6. λx.f(x) ∈ I ⟶ℝ
⊢ ∃y:ℝ. inf(f(x)(x∈I)) = y
BY
{ (FLemma `totally-bounded-inf` [4]⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  I  :  \{I:Interval|  icompact(I)\}  @i
2.  f  :  I  {}\mrightarrow{}\mBbbR{}@i
3.  f(x)  continuous  for  x  \mmember{}  I@i
4.  totally-bounded(f(x)(x\mmember{}I))
5.  icompact(I)
6.  \mlambda{}x.f(x)  \mmember{}  I  {}\mrightarrow{}\mBbbR{}
\mvdash{}  \mexists{}y:\mBbbR{}.  inf(f(x)(x\mmember{}I))  =  y


By

---

Latex:
(FLemma  `totally-bounded-inf`  [4]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index