---

Step * of Lemma compact-dist-zero

∀[X:Type]
  ∀d:metric(X). ∀A:Type.
    ∀c:mcompact(A;d). ∀x:X.  (dist(x;A) = r0 ⇐⇒ ∀n:ℕ+. ∃a:A. (mdist(d;x;a) < (r1/r(n)))) supposing A ⊆r X
BY
{ ((UnivCD THENA Auto)
   THEN (Assert dist-fun(d;x) ∈ FUN(A ⟶ ℝ) BY
               (DoSubsume THEN 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 (RepeatFor 2 (D 0) THENA ((RepeatFor 2 (D 0) THEN Try ((Assert a ∈ X BY Auto)) THEN Auto) ORELSE Auto))) }

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. ∀x@0:A. (dist(x;A) ≤ (dist-fun(d;x) x@0))
9. ∀e:ℝ. ((r0 < e) ⇒ (∃x@0:A. ((dist-fun(d;x) x@0) < (dist(x;A) + e))))
10. dist(x;A) = r0
⊢ ∀n:ℕ+. ∃a:A. (mdist(d;x;a) < (r1/r(n)))

2
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. ∀x@0:A. (dist(x;A) ≤ (dist-fun(d;x) x@0))
9. ∀e:ℝ. ((r0 < e) ⇒ (∃x@0:A. ((dist-fun(d;x) x@0) < (dist(x;A) + e))))
10. ∀n:ℕ+. ∃a:A. (mdist(d;x;a) < (r1/r(n)))
⊢ dist(x;A) = r0

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}A:Type.
        \mforall{}c:mcompact(A;d).  \mforall{}x:X.    (dist(x;A)  =  r0  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}a:A.  (mdist(d;x;a)  <  (r1/r(n)))) 
        supposing  A  \msubseteq{}r  X


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  dist-fun(d;x)  \mmember{}  FUN(A  {}\mrightarrow{}  \mBbbR{})  BY
                          (DoSubsume  THEN  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  (RepeatFor  2  (D  0)
              THENA  ((RepeatFor  2  (D  0)  THEN  Try  ((Assert  a  \mmember{}  X  BY  Auto))  THEN  Auto)  ORELSE  Auto)
              ))

---

Home Index