---

Step * of Lemma inf-range

∀I:{I:Interval| icompact(I)} . ∀f:I ⟶ℝ.  (f[x] continuous for x ∈ I ⇒ (∃y:ℝ. inf(f(x)(x∈I)) = y))
BY
{ (InstLemma `continuous-compact-range-totally-bounded` []
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN D -1
   THEN Auto
   THEN (Assert icompact(I) BY
               Auto)
   THEN All (\h. Unfold `so_apply` h THEN Fold `r-ap` h)⋅
   THEN (Assert λx.f(x) ∈ I ⟶ℝ BY
               (Auto THEN D (-1) THEN Unhide THEN Auto))) }

1
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

---

Latex:

---

Latex:
\mforall{}I:\{I:Interval|  icompact(I)\}  .  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.    (f[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  (\mexists{}y:\mBbbR{}.  inf(f(x)(x\mmember{}I))  =  y))


By

---

Latex:
(InstLemma  `continuous-compact-range-totally-bounded`  []
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  D  -1
  THEN  Auto
  THEN  (Assert  icompact(I)  BY
                          Auto)
  THEN  All  (\mbackslash{}h.  Unfold  `so\_apply`  h  THEN  Fold  `r-ap`  h)\mcdot{}
  THEN  (Assert  \mlambda{}x.f(x)  \mmember{}  I  {}\mrightarrow{}\mBbbR{}  BY
                          (Auto  THEN  D  (-1)  THEN  Unhide  THEN  Auto)))

---

Home Index