Step * 1 1 1 of Lemma mcompact-stable-union


1. [X] Type
2. metric(X)
3. [T] Type
4. [P] T ⟶ X ⟶ ℙ
5. [%] : ∀i:T. ∀x,y:X.  (P[i;x]  y ≡  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
11. ∀i:T. m-TB({x:X| P[i;x]} ;d)
12. : ℕ
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 i1) ≤ (r1/r((2 (k 1)) 1)))
16. : ℕ
17. i:T × ℕsz ~ ℕn
18. : ℕn ⟶ (i:T × ℕsz i)
19. Bij(ℕn;i:T × ℕsz i;f)
20. 0 < n
21. λj.let i,a 
       in pts a ∈ ℕn ⟶ stable-union(X;T;i,x.P[i;x])
22. X
23. ¬¬(∃i:T. P[i;x])
⊢ ∃i:ℕn. (mdist(d;x;(λj.let i,a in pts a) i) ≤ (r1/r(k 1)))
BY
(Assert ∀i:ℕn
            (((r1/r((2 (k 1)) 1)) < mdist(d;x;(λj.let i,a in pts a) i))
            ∨ (mdist(d;x;(λj.let i,a in pts a) i) < (r1/r(k 1)))) BY
         (Auto
          THEN (GenConclTerm ⌜λj.let i,a in pts a⌝⋅ THENA Auto)
          THEN (GenConclTerm ⌜i⌝⋅ THENA Auto)
          THEN -2
          THEN BLemma `rless-cases`
          THEN Auto)) }

1
1. [X] Type
2. metric(X)
3. [T] Type
4. [P] T ⟶ X ⟶ ℙ
5. [%] : ∀i:T. ∀x,y:X.  (P[i;x]  y ≡  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
11. ∀i:T. m-TB({x:X| P[i;x]} ;d)
12. : ℕ
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 i1) ≤ (r1/r((2 (k 1)) 1)))
16. : ℕ
17. i:T × ℕsz ~ ℕn
18. : ℕn ⟶ (i:T × ℕsz i)
19. Bij(ℕn;i:T × ℕsz i;f)
20. 0 < n
21. λj.let i,a 
       in pts a ∈ ℕn ⟶ stable-union(X;T;i,x.P[i;x])
22. X
23. ¬¬(∃i:T. P[i;x])
24. ∀i:ℕn
      (((r1/r((2 (k 1)) 1)) < mdist(d;x;(λj.let i,a in pts a) i))
      ∨ (mdist(d;x;(λj.let i,a in pts a) i) < (r1/r(k 1))))
⊢ ∃i:ℕn. (mdist(d;x;(λj.let i,a in pts 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.  f  :  \mBbbN{}n  {}\mrightarrow{}  (i:T  \mtimes{}  \mBbbN{}sz  i)
19.  Bij(\mBbbN{}n;i:T  \mtimes{}  \mBbbN{}sz  i;f)
20.  0  <  n
21.  \mlambda{}j.let  i,a  =  f  j 
              in  pts  i  a  \mmember{}  \mBbbN{}n  {}\mrightarrow{}  stable-union(X;T;i,x.P[i;x])
22.  x  :  X
23.  \mneg{}\mneg{}(\mexists{}i:T.  P[i;x])
\mvdash{}  \mexists{}i:\mBbbN{}n.  (mdist(d;x;(\mlambda{}j.let  i,a  =  f  j  in  pts  i  a)  i)  \mleq{}  (r1/r(k  +  1)))


By


Latex:
(Assert  \mforall{}i:\mBbbN{}n
                    (((r1/r((2  *  (k  +  1))  +  1))  <  mdist(d;x;(\mlambda{}j.let  i,a  =  f  j  in  pts  i  a)  i))
                    \mvee{}  (mdist(d;x;(\mlambda{}j.let  i,a  =  f  j  in  pts  i  a)  i)  <  (r1/r(k  +  1))))  BY
              (Auto
                THEN  (GenConclTerm  \mkleeneopen{}\mlambda{}j.let  i,a  =  f  j  in  pts  i  a\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (GenConclTerm  \mkleeneopen{}v  i\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  D  -2
                THEN  BLemma  `rless-cases`
                THEN  Auto))




Home Index