---

Step * 1 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)))
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)))
BY
{ (D -2
   THEN (Assert λj.let i,a = f j 
                   in pts i a ∈ ℕn ⟶ stable-union(X;T;i,x.P[i;x]) BY
               ((FunExt THENA Auto)
                THEN Reduce 0
                THEN (GenConclAtAddr [2;1] THEN D -2)
                THEN Reduce 0
                THEN DoSubsume
                THEN Auto
                THEN (D 0 THENA Auto)
                THEN D -1
                THEN MemTypeCD
                THEN Auto))
   THEN D 0 With ⌜λj.let i,a = f j 
                     in pts i a⌝ 
   THEN Auto
   THEN D -1
   THEN (Assert ¬¬(∃i:T. P[i;x]) BY
               Auto)
   THEN Thin (-2)) }

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. f : ℕn ⟶ (i:T × ℕsz i)
19. Bij(ℕn;i:T × ℕsz i;f)
20. 0 < n
21. λj.let i,a = f j 
       in pts i a ∈ ℕn ⟶ stable-union(X;T;i,x.P[i;x])
22. x : X
23. ¬¬(∃i:T. P[i;x])
⊢ ∃i:ℕn. (mdist(d;x;(λj.let i,a = f j in pts i a) 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)))
16.  n  :  \mBbbN{}
17.  i:T  \mtimes{}  \mBbbN{}sz  i  \msim{}  \mBbbN{}n
18.  \mBbbN{}n  \msim{}  i:T  \mtimes{}  \mBbbN{}sz  i
19.  0  <  n
\mvdash{}  \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:
(D  -2
  THEN  (Assert  \mlambda{}j.let  i,a  =  f  j 
                                  in  pts  i  a  \mmember{}  \mBbbN{}n  {}\mrightarrow{}  stable-union(X;T;i,x.P[i;x])  BY
                          ((FunExt  THENA  Auto)
                            THEN  Reduce  0
                            THEN  (GenConclAtAddr  [2;1]  THEN  D  -2)
                            THEN  Reduce  0
                            THEN  DoSubsume
                            THEN  Auto
                            THEN  (D  0  THENA  Auto)
                            THEN  D  -1
                            THEN  MemTypeCD
                            THEN  Auto))
  THEN  D  0  With  \mkleeneopen{}\mlambda{}j.let  i,a  =  f  j 
                                      in  pts  i  a\mkleeneclose{} 
  THEN  Auto
  THEN  D  -1
  THEN  (Assert  \mneg{}\mneg{}(\mexists{}i:T.  P[i;x])  BY
                          Auto)
  THEN  Thin  (-2))

---

Home Index