---

Step * of Lemma compact-inf-property

∀[X:Type]
  ∀d:metric(X). ∀c:mcompact(X;d). ∀f:FUN(X ⟶ ℝ).
    ((∀x:X. (compact-inf{i:l}(d;c;f) ≤ (f x))) ∧ (∀e:ℝ. ((r0 < e) ⇒ (∃x:X. ((f x) < (compact-inf{i:l}(d;c;f) + e))))))
BY
{ (Intros
   THEN (InstLemma `m-inf-property` [⌜X⌝;⌜d⌝;⌜snd(c)⌝;⌜f⌝; ⌜compact-mc{i:l}(d;c;f)⌝] ⋅ THENA Auto)
   THEN Fold `compact-inf` (-1)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}c:mcompact(X;d).  \mforall{}f:FUN(X  {}\mrightarrow{}  \mBbbR{}).
        ((\mforall{}x:X.  (compact-inf\{i:l\}(d;c;f)  \mleq{}  (f  x)))
        \mwedge{}  (\mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:X.  ((f  x)  <  (compact-inf\{i:l\}(d;c;f)  +  e))))))


By

---

Latex:
(Intros
  THEN  (InstLemma  `m-inf-property`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}snd(c)\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}compact-mc\{i:l\}(d;c;f)\mkleeneclose{}]  \mcdot{}  THENA  Auto)
  THEN  Fold  `compact-inf`  (-1)
  THEN  Trivial)

---

Home Index