---

Step * 1 1 of Lemma range-inf_wf


1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f x continuous for x ∈ I
⊢ TERMOF{inf-range:o, 1:l} I (λx.(f x)) ∈ f x continuous for x ∈ I ⟶ (∃y:ℝ. inf(f x(x∈I)) = y)
BY
{ (GenConclAtAddr [2;1] THEN RepUR ``so_apply r-ap`` -2 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  mc  :  f  x  continuous  for  x  \mmember{}  I
\mvdash{}  TERMOF\{inf-range:o,  1:l\}  I  (\mlambda{}x.(f  x))  \mmember{}  f  x  continuous  for  x  \mmember{}  I  {}\mrightarrow{}  (\mexists{}y:\mBbbR{}.  inf(f  x(x\mmember{}I))  =  y)


By

---

Latex:
(GenConclAtAddr  [2;1]  THEN  RepUR  ``so\_apply  r-ap``  -2  THEN  Auto)

---

Home Index