---

Step * of Lemma not-in-compact-separated

No Annotations
∀[X:Type]
  ∀d:metric(X)
    ∀[A:Type]
      ∀c:mcompact(A;d). ∀x:X.  (¬(x ∈ A) ⇐⇒ ¬¬(∃n:ℕ+. ∀a:A. ((r1/r(n)) ≤ mdist(d;x;a)))) 
      supposing mcomplete(X with d) ∧ metric-subspace(X;d;A)
BY
{ (RepeatFor 4 (Intro)
   THEN (Assert metric-subspace(X;d;A) BY
               (Unhide THEN Auto))
   THEN D -1
   THEN (RWO "strong-subtype-iff-respects-equality" 5 THENA Auto)
   THEN D -2
   THEN Intros
   THEN (RepeatFor 2 (D 0) THENA (RepeatFor 4 (D 0) THEN Try ((Assert a ∈ X BY Auto)) THEN Auto))) }

1
1. [X] : Type
2. d : metric(X)
3. [A] : Type
4. [%] : mcomplete(X with d) ∧ metric-subspace(X;d;A)
5. A ⊆r X
6. respects-equality(X;A)
7. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
8. c : mcompact(A;d)
9. x : X
10. ¬(x ∈ A)
⊢ ¬¬(∃n:ℕ+. ∀a:A. ((r1/r(n)) ≤ mdist(d;x;a)))

2
1. [X] : Type
2. d : metric(X)
3. [A] : Type
4. [%] : mcomplete(X with d) ∧ metric-subspace(X;d;A)
5. A ⊆r X
6. respects-equality(X;A)
7. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
8. c : mcompact(A;d)
9. x : X
10. ¬¬(∃n:ℕ+. ∀a:A. ((r1/r(n)) ≤ mdist(d;x;a)))
⊢ ¬(x ∈ A)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type]
    \mforall{}d:metric(X)
        \mforall{}[A:Type]
            \mforall{}c:mcompact(A;d).  \mforall{}x:X.    (\mneg{}(x  \mmember{}  A)  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}a:A.  ((r1/r(n))  \mleq{}  mdist(d;x;a)))) 
            supposing  mcomplete(X  with  d)  \mwedge{}  metric-subspace(X;d;A)


By

---

Latex:
(RepeatFor  4  (Intro)
  THEN  (Assert  metric-subspace(X;d;A)  BY
                          (Unhide  THEN  Auto))
  THEN  D  -1
  THEN  (RWO  "strong-subtype-iff-respects-equality"  5  THENA  Auto)
  THEN  D  -2
  THEN  Intros
  THEN  (RepeatFor  2  (D  0)  THENA  (RepeatFor  4  (D  0)  THEN  Try  ((Assert  a  \mmember{}  X  BY  Auto))  THEN  Auto)))

---

Home Index