---

Step * 1 of Lemma mcompact-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. mcomplete(X with d)
8. ∀i:T. mcompact({x:X| P[i;x]} ;d)
9. mcomplete(stable-union(X;T;i,x.P[i;x]) with d)
10. t : T
11. ∀i:T. m-TB({x:X| P[i;x]} ;d)
12. k : ℕ
13. sz : i:T ⟶ ℕ+
14. pts : i:T ⟶ ℕsz i ⟶ {x:X| P[i;x]} 
15. ∀i:T. ∀x:{x:X| P[i;x]} .  ∃i1:ℕsz i. (mdist(d;x;pts i i1) ≤ (r1/r((2 * (k + 1)) + 1)))
⊢ ∃n:ℕ+
   ∃xs:ℕn ⟶ stable-union(X;T;i,x.P[i;x]). ∀x:stable-union(X;T;i,x.P[i;x]). ∃i:ℕn. (mdist(d;x;xs i) ≤ (r1/r(k + 1)))
BY
{ ((Assert finite(i:T × ℕsz i) BY
          (BLemma `finite-product` ⋅ THEN Auto))
   THEN D -1
   THEN (Assert ℕn ~ i:T × ℕsz i BY
               EAuto 1)
   THEN (Assert 0 < n BY
               (SupposeNot THEN D -3 THEN (Assert f <t, 0> ∈ ℕn BY Auto) THEN Auto))
   THEN (D 0 With ⌜n⌝  THENW 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. mcomplete(X with d)
8. ∀i:T. mcompact({x:X| P[i;x]} ;d)
9. mcomplete(stable-union(X;T;i,x.P[i;x]) with d)
10. t : T
11. ∀i:T. m-TB({x:X| P[i;x]} ;d)
12. k : ℕ
13. sz : i:T ⟶ ℕ+
14. pts : i:T ⟶ ℕsz i ⟶ {x:X| P[i;x]} 
15. ∀i:T. ∀x:{x:X| P[i;x]} .  ∃i1:ℕsz i. (mdist(d;x;pts i i1) ≤ (r1/r((2 * (k + 1)) + 1)))
16. n : ℕ
17. i:T × ℕsz i ~ ℕn
18. ℕn ~ i:T × ℕsz i
19. 0 < n
⊢ ∃xs:ℕn ⟶ stable-union(X;T;i,x.P[i;x]). ∀x:stable-union(X;T;i,x.P[i;x]). ∃i:ℕn. (mdist(d;x;xs i) ≤ (r1/r(k + 1)))

---

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.  mcomplete(X  with  d)
8.  \mforall{}i:T.  mcompact(\{x:X|  P[i;x]\}  ;d)
9.  mcomplete(stable-union(X;T;i,x.P[i;x])  with  d)
10.  t  :  T
11.  \mforall{}i:T.  m-TB(\{x:X|  P[i;x]\}  ;d)
12.  k  :  \mBbbN{}
13.  sz  :  i:T  {}\mrightarrow{}  \mBbbN{}\msupplus{}
14.  pts  :  i:T  {}\mrightarrow{}  \mBbbN{}sz  i  {}\mrightarrow{}  \{x:X|  P[i;x]\} 
15.  \mforall{}i:T.  \mforall{}x:\{x:X|  P[i;x]\}  .    \mexists{}i1:\mBbbN{}sz  i.  (mdist(d;x;pts  i  i1)  \mleq{}  (r1/r((2  *  (k  +  1))  +  1)))
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}
      \mexists{}xs:\mBbbN{}n  {}\mrightarrow{}  stable-union(X;T;i,x.P[i;x])
        \mforall{}x:stable-union(X;T;i,x.P[i;x]).  \mexists{}i:\mBbbN{}n.  (mdist(d;x;xs  i)  \mleq{}  (r1/r(k  +  1)))


By

---

Latex:
((Assert  finite(i:T  \mtimes{}  \mBbbN{}sz  i)  BY
                (BLemma  `finite-product`  \mcdot{}  THEN  Auto))
  THEN  D  -1
  THEN  (Assert  \mBbbN{}n  \msim{}  i:T  \mtimes{}  \mBbbN{}sz  i  BY
                          EAuto  1)
  THEN  (Assert  0  <  n  BY
                          (SupposeNot  THEN  D  -3  THEN  (Assert  f  <t,  0>  \mmember{}  \mBbbN{}n  BY  Auto)  THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}n\mkleeneclose{}    THENW  Auto))

---

Home Index