---

Step * of Lemma m-TB-sup-and-inf

∀[X:Type]
  ∀dX:metric(X)
    (m-TB(X;dX)
    ⇒ (∀f:X ⟶ ℝ. (UC(f:X ⟶ ℝ) ⇒ ((∃a:ℝ. inf(λr.∃x:X. (r = (f x))) = a) ∧ (∃b:ℝ. sup(λr.∃x:X. (r = (f x))) = b)))))
BY
{ (Intros
   THEN (InstLemma `continuous-image-m-TB` [⌜X⌝;⌜dX⌝;⌜ℝ⌝;⌜rmetric()⌝;⌜f⌝]⋅ THENA Auto)
   THEN (Assert λr.∃x:X. (r = (f x)) ∈ Set(ℝ) BY
               (MemTypeCD THEN Reduce 0 THEN Auto))
   THEN (Assert ⌜totally-bounded(λr.∃x:X. (r = (f x)))⌝⋅
   THENM (D 0 THEN (BLemma `totally-bounded-sup` ORELSE BLemma `totally-bounded-inf`) THEN Auto)
   )) }

1
.....assertion..... 
1. [X] : Type
2. dX : metric(X)
3. m-TB(X;dX)
4. f : X ⟶ ℝ
5. UC(f:X ⟶ ℝ)
6. m-TB(f[X];image-metric(rmetric()))
7. λr.∃x:X. (r = (f x)) ∈ Set(ℝ)
⊢ totally-bounded(λr.∃x:X. (r = (f x)))

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}dX:metric(X)
        (m-TB(X;dX)
        {}\mRightarrow{}  (\mforall{}f:X  {}\mrightarrow{}  \mBbbR{}
                    (UC(f:X  {}\mrightarrow{}  \mBbbR{})
                    {}\mRightarrow{}  ((\mexists{}a:\mBbbR{}.  inf(\mlambda{}r.\mexists{}x:X.  (r  =  (f  x)))  =  a)  \mwedge{}  (\mexists{}b:\mBbbR{}.  sup(\mlambda{}r.\mexists{}x:X.  (r  =  (f  x)))  =  b)))))


By

---

Latex:
(Intros
  THEN  (InstLemma  `continuous-image-m-TB`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}dX\mkleeneclose{};\mkleeneopen{}\mBbbR{}\mkleeneclose{};\mkleeneopen{}rmetric()\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mlambda{}r.\mexists{}x:X.  (r  =  (f  x))  \mmember{}  Set(\mBbbR{})  BY
                          (MemTypeCD  THEN  Reduce  0  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}totally-bounded(\mlambda{}r.\mexists{}x:X.  (r  =  (f  x)))\mkleeneclose{}\mcdot{}
  THENM  (D  0  THEN  (BLemma  `totally-bounded-sup`  ORELSE  BLemma  `totally-bounded-inf`)  THEN  Auto)
  ))

---

Home Index