---

Step * of Lemma compact-sup-property

∀[X:Type]
  ∀d:metric(X). ∀c:mcompact(X;d). ∀f:FUN(X ⟶ ℝ).
    ((∀x:X. ((f x) ≤ compact-sup{i:l}(d;c;f))) ∧ (∀e:ℝ. ((r0 < e) ⇒ (∃x:X. ((compact-sup{i:l}(d;c;f) - e) < (f x))))))
BY
{ (Intros
   THEN (InstLemma `m-sup-property` [⌜X⌝;⌜d⌝;⌜snd(c)⌝;⌜f⌝; ⌜compact-mc{i:l}(d;c;f)⌝] ⋅ THENA Auto)
   THEN Fold `compact-sup` (-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.  ((f  x)  \mleq{}  compact-sup\{i:l\}(d;c;f)))
        \mwedge{}  (\mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:X.  ((compact-sup\{i:l\}(d;c;f)  -  e)  <  (f  x))))))


By

---

Latex:
(Intros
  THEN  (InstLemma  `m-sup-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-sup`  (-1)
  THEN  Trivial)

---

Home Index