---

Step * of Lemma compact-dist-nonneg

∀[X:Type]. ∀[d:metric(X)]. ∀[A:Type].  ∀[c:mcompact(A;d)]. ∀[x:X].  (r0 ≤ dist(x;A)) supposing A ⊆r X
BY
{ (Auto
   THEN (Assert dist-fun(d;x) ∈ FUN(A ⟶ ℝ) BY
               (DoSubsume THEN Auto))
   THEN (BLemma `not-rless` THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (InstLemma `compact-inf-property` [⌜A⌝;⌜d⌝;⌜c⌝;⌜dist-fun(d;x)⌝]⋅ THENA Auto)
   THEN (Subst' compact-inf{i:l}(d;c;dist-fun(d;x)) ~ dist(x;A) -1 THENA (RepUR ``compact-dist`` 0 THEN Auto))
   THEN D -1
   THEN (InstHyp [⌜-(dist(x;A))⌝] (-1)⋅ THENA Auto)
   THEN ExRepD) }

1
1. X : Type
2. d : metric(X)
3. A : Type
4. A ⊆r X
5. c : mcompact(A;d)
6. x : X
7. dist-fun(d;x) ∈ FUN(A ⟶ ℝ)
8. dist(x;A) < r0
9. ∀x@0:A. (dist(x;A) ≤ (dist-fun(d;x) x@0))
10. ∀e:ℝ. ((r0 < e) ⇒ (∃x@0:A. ((dist-fun(d;x) x@0) < (dist(x;A) + e))))
11. x@0 : A
12. (dist-fun(d;x) x@0) < (dist(x;A) + -(dist(x;A)))
⊢ False

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[A:Type].
    \mforall{}[c:mcompact(A;d)].  \mforall{}[x:X].    (r0  \mleq{}  dist(x;A))  supposing  A  \msubseteq{}r  X


By

---

Latex:
(Auto
  THEN  (Assert  dist-fun(d;x)  \mmember{}  FUN(A  {}\mrightarrow{}  \mBbbR{})  BY
                          (DoSubsume  THEN  Auto))
  THEN  (BLemma  `not-rless`  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `compact-inf-property`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}dist-fun(d;x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  compact-inf\{i:l\}(d;c;dist-fun(d;x))  \msim{}  dist(x;A)  -1
              THENA  (RepUR  ``compact-dist``  0  THEN  Auto)
              )
  THEN  D  -1
  THEN  (InstHyp  [\mkleeneopen{}-(dist(x;A))\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index