---

Step * of Lemma compact-dist-positive

∀[X:Type]
  ∀d:metric(X). ∀A:Type.
    ∀c:mcompact(A;d). ∀x:X.  (r0 < dist(x;A) ⇐⇒ ∃n:ℕ+. ∀a:A. ((r1/r(n)) ≤ mdist(d;x;a))) 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 (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))) ∧ (∀e:ℝ. ((r0 < e) ⇒ (∃x@0:A. ((dist-fun(d;x) x@0) < (dist(x;A) + e)))))
9. r0 < dist(x;A)
⊢ ∃n:ℕ+. ∀a:A. ((r1/r(n)) ≤ mdist(d;x;a))

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

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}A:Type.
        \mforall{}c:mcompact(A;d).  \mforall{}x:X.    (r0  <  dist(x;A)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}a:A.  ((r1/r(n))  \mleq{}  mdist(d;x;a))) 
        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  (RepeatFor  2  (D  0)
              THENA  ((RepeatFor  2  (D  0)  THEN  Try  ((Assert  a  \mmember{}  X  BY  Auto))  THEN  Auto)  ORELSE  Auto)
              ))

---

Home Index