---

Step * 2 1 of Lemma mcomplete-stable-union


1. X : Type
2. d : metric(X)
3. T : Type
4. P : T ⟶ X ⟶ ℙ
5. ∀i:T. ∀x,y:X.  (P[i;x] ⇒ y ≡ x ⇒ P[i;y])
6. finite(T)
7. ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
8. cmp : ∀i:T. mcompact({x:X| P[i;x]} ;d)
9. x : ℕ ⟶ stable-union(X;T;i,x.P[i;x])
10. mcauchy(d;n.x n)
11. y : X
12. lim n→∞.x n = y
13. i : T
14. ¬(r0 < dist(y;{x:X| P[i;x]} ))
15. dist(y;{x:X| P[i;x]} ) ≤ r0
16. r0 ≤ dist(y;{x:X| P[i;x]} )
17. ∀n:ℕ+. ∃a:{x:X| P[i;x]} . (mdist(d;y;a) < (r1/r(n)))
⊢ ¬¬P[i;y]
BY
{ ((InstLemma `m-closed-iff-complete` [⌜X⌝;⌜d⌝;⌜{x:X| P[i;x]} ⌝]⋅ THENA (Auto THEN EAuto 1))
   THEN (RepeatFor 2 (D -1) THENA ((Assert mcompact({x:X| P[i;x]} ;d) BY BackThruSomeHyp) THEN D -1 THEN Auto))
   ) }

1
1. X : Type
2. d : metric(X)
3. T : Type
4. P : T ⟶ X ⟶ ℙ
5. ∀i:T. ∀x,y:X.  (P[i;x] ⇒ y ≡ x ⇒ P[i;y])
6. finite(T)
7. ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
8. cmp : ∀i:T. mcompact({x:X| P[i;x]} ;d)
9. x : ℕ ⟶ stable-union(X;T;i,x.P[i;x])
10. mcauchy(d;n.x n)
11. y : X
12. lim n→∞.x n = y
13. i : T
14. ¬(r0 < dist(y;{x:X| P[i;x]} ))
15. dist(y;{x:X| P[i;x]} ) ≤ r0
16. r0 ≤ dist(y;{x:X| P[i;x]} )
17. ∀n:ℕ+. ∃a:{x:X| P[i;x]} . (mdist(d;y;a) < (r1/r(n)))
18. m-closed-subspace(X;d;{x:X| P[i;x]} ) ⇒ mcomplete({x:X| P[i;x]}  with d)
19. m-closed-subspace(X;d;{x:X| P[i;x]} )
⊢ ¬¬P[i;y]

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  T  :  Type
4.  P  :  T  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}i:T.  \mforall{}x,y:X.    (P[i;x]  {}\mRightarrow{}  y  \mequiv{}  x  {}\mRightarrow{}  P[i;y])
6.  finite(T)
7.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  (mcauchy(d;n.x  n)  {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})
8.  cmp  :  \mforall{}i:T.  mcompact(\{x:X|  P[i;x]\}  ;d)
9.  x  :  \mBbbN{}  {}\mrightarrow{}  stable-union(X;T;i,x.P[i;x])
10.  mcauchy(d;n.x  n)
11.  y  :  X
12.  lim  n\mrightarrow{}\minfty{}.x  n  =  y
13.  i  :  T
14.  \mneg{}(r0  <  dist(y;\{x:X|  P[i;x]\}  ))
15.  dist(y;\{x:X|  P[i;x]\}  )  \mleq{}  r0
16.  r0  \mleq{}  dist(y;\{x:X|  P[i;x]\}  )
17.  \mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}a:\{x:X|  P[i;x]\}  .  (mdist(d;y;a)  <  (r1/r(n)))
\mvdash{}  \mneg{}\mneg{}P[i;y]


By

---

Latex:
((InstLemma  `m-closed-iff-complete`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}\{x:X|  P[i;x]\}  \mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  EAuto  1))
  THEN  (RepeatFor  2  (D  -1)  THENA  ((Assert  mcompact(\{x:X|  P[i;x]\}  ;d)  BY  BackThruSomeHyp)  THEN  D  -1  TH\000CEN  Auto))
  )

---

Home Index