---

Step * of Lemma m-closed-iff-complete

∀[X:Type]
  ∀d:metric(X)
    (mcomplete(X with d) ⇒ (∀[A:Type]. (metric-subspace(X;d;A) ⇒ (m-closed-subspace(X;d;A) ⇐⇒ mcomplete(A with d)))))
BY
{ (RepeatFor 5 (Intro)
   THEN (Assert d ∈ metric(A) BY
               (D -1 THEN D 2 THEN MemTypeCD THEN Auto))
   THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. [X] : Type
2. d : metric(X)
3. mcomplete(X with d)
4. [A] : Type
5. metric-subspace(X;d;A)
6. d ∈ metric(A)
7. m-closed-subspace(X;d;A)
⊢ mcomplete(A with d)

2
1. [X] : Type
2. d : metric(X)
3. mcomplete(X with d)
4. [A] : Type
5. metric-subspace(X;d;A)
6. d ∈ metric(A)
7. mcomplete(A with d)
⊢ m-closed-subspace(X;d;A)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X)
        (mcomplete(X  with  d)
        {}\mRightarrow{}  (\mforall{}[A:Type].  (metric-subspace(X;d;A)  {}\mRightarrow{}  (m-closed-subspace(X;d;A)  \mLeftarrow{}{}\mRightarrow{}  mcomplete(A  with  d)))))


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  (Assert  d  \mmember{}  metric(A)  BY
                          (D  -1  THEN  D  2  THEN  MemTypeCD  THEN  Auto))
  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index