---

Step * 1 1 1 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. n : ℕ
7. T ~ ℕn
8. ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
9. cmp : ∀i:T. mcompact({x:X| P[i;x]} ;d)
10. x : ℕ ⟶ stable-union(X;T;i,x.P[i;x])
11. mcauchy(d;n.x n)
12. y : X
13. lim n→∞.x n = y
14. ∀i:T. ∃n:ℕ+. ∀a:{x:X| P[i;x]} . ((r1/r(n)) ≤ mdist(d;y;a))
15. f : ℕn ⟶ T
16. Bij(ℕn;T;f)
⊢ ∃n:ℕ+. ∀i:T. ∀a:{x:X| P[i;x]} .  ((r1/r(n)) ≤ mdist(d;y;a))
BY
{ ((Assert ∀i:ℕn. ∃n:ℕ+. ∀a:{x:X| P[f i;x]} . ((r1/r(n)) ≤ mdist(d;y;a)) BY
          Auto)
   THEN (Skolemize (-1) `b' THENA ((RepeatFor 2 (D 0) THEN DSetVars THEN Auto) ORELSE 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. n : ℕ
7. T ~ ℕn
8. ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
9. cmp : ∀i:T. mcompact({x:X| P[i;x]} ;d)
10. x : ℕ ⟶ stable-union(X;T;i,x.P[i;x])
11. mcauchy(d;n.x n)
12. y : X
13. lim n→∞.x n = y
14. ∀i:T. ∃n:ℕ+. ∀a:{x:X| P[i;x]} . ((r1/r(n)) ≤ mdist(d;y;a))
15. f : ℕn ⟶ T
16. Bij(ℕn;T;f)
17. ∀i:ℕn. ∃n:ℕ+. ∀a:{x:X| P[f i;x]} . ((r1/r(n)) ≤ mdist(d;y;a))
18. b : i:ℕn ⟶ ℕ+
19. ∀i:ℕn. ∀a:{x:X| P[f i;x]} .  ((r1/r(b i)) ≤ mdist(d;y;a))
⊢ ∃n:ℕ+. ∀i:T. ∀a:{x:X| P[i;x]} .  ((r1/r(n)) ≤ mdist(d;y;a))

---

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.  n  :  \mBbbN{}
7.  T  \msim{}  \mBbbN{}n
8.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  (mcauchy(d;n.x  n)  {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})
9.  cmp  :  \mforall{}i:T.  mcompact(\{x:X|  P[i;x]\}  ;d)
10.  x  :  \mBbbN{}  {}\mrightarrow{}  stable-union(X;T;i,x.P[i;x])
11.  mcauchy(d;n.x  n)
12.  y  :  X
13.  lim  n\mrightarrow{}\minfty{}.x  n  =  y
14.  \mforall{}i:T.  \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}a:\{x:X|  P[i;x]\}  .  ((r1/r(n))  \mleq{}  mdist(d;y;a))
15.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
16.  Bij(\mBbbN{}n;T;f)
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}i:T.  \mforall{}a:\{x:X|  P[i;x]\}  .    ((r1/r(n))  \mleq{}  mdist(d;y;a))


By

---

Latex:
((Assert  \mforall{}i:\mBbbN{}n.  \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}a:\{x:X|  P[f  i;x]\}  .  ((r1/r(n))  \mleq{}  mdist(d;y;a))  BY
                Auto)
  THEN  (Skolemize  (-1)  `b'  THENA  ((RepeatFor  2  (D  0)  THEN  DSetVars  THEN  Auto)  ORELSE  Auto))
  )

---

Home Index