---

Step * of Lemma mcompact-stable-union

∀[X:Type]
  ∀d:metric(X)
    ∀[T:Type]. ∀[P:T ⟶ X ⟶ ℙ].
      finite(T) ⇒ mcomplete(X with d) ⇒ (∀i:T. mcompact({x:X| P[i;x]} ;d)) ⇒ T ⇒ mcompact(stable-union(X;T;i,x.P[i;x\000C]);d) 
      supposing ∀i:T. ∀x,y:X.  (P[i;x] ⇒ y ≡ x ⇒ P[i;y])
BY
{ (InstLemma `mcomplete-stable-union` []
   THEN RepeatFor 8 ((ParallelLast' THENA Auto))
   THEN ((D 0 THENA Auto) THEN RenameVar `t' (-1))
   THEN D 0
   THEN Try (Trivial)
   THEN (Assert ∀i:T. m-TB({x:X| P[i;x]} ;d) BY
               (ParallelOp -3 THEN D -1 THEN Auto))
   THEN RWO "m-TB-iff" 0
   THEN Auto
   THEN (Assert ∀i:T
                  ∃n:ℕ+
                   ∃xs:ℕn ⟶ {x:X| P[i;x]} . ∀x:{x:X| P[i;x]} . ∃i:ℕn. (mdist(d;x;xs i) ≤ (r1/r((2 * (k + 1)) + 1))) BY
               (ParallelOp -2 THEN RWO "m-TB-iff" (-1) THEN Auto))
   THEN ((Skolemize (-1) `sz' THENA Auto) THEN Thin (-3))
   THEN (Skolemize (-1) `pts' THENA Auto)
   THEN Thin (-3)) }

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)))
⊢ ∃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:
\mforall{}[X:Type]
    \mforall{}d:metric(X)
        \mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}].
            finite(T)
            {}\mRightarrow{}  mcomplete(X  with  d)
            {}\mRightarrow{}  (\mforall{}i:T.  mcompact(\{x:X|  P[i;x]\}  ;d))
            {}\mRightarrow{}  T
            {}\mRightarrow{}  mcompact(stable-union(X;T;i,x.P[i;x]);d) 
            supposing  \mforall{}i:T.  \mforall{}x,y:X.    (P[i;x]  {}\mRightarrow{}  y  \mequiv{}  x  {}\mRightarrow{}  P[i;y])


By

---

Latex:
(InstLemma  `mcomplete-stable-union`  []
  THEN  RepeatFor  8  ((ParallelLast'  THENA  Auto))
  THEN  ((D  0  THENA  Auto)  THEN  RenameVar  `t'  (-1))
  THEN  D  0
  THEN  Try  (Trivial)
  THEN  (Assert  \mforall{}i:T.  m-TB(\{x:X|  P[i;x]\}  ;d)  BY
                          (ParallelOp  -3  THEN  D  -1  THEN  Auto))
  THEN  RWO  "m-TB-iff"  0
  THEN  Auto
  THEN  (Assert  \mforall{}i:T
                                \mexists{}n:\mBbbN{}\msupplus{}
                                  \mexists{}xs:\mBbbN{}n  {}\mrightarrow{}  \{x:X|  P[i;x]\} 
                                    \mforall{}x:\{x:X|  P[i;x]\}  .  \mexists{}i:\mBbbN{}n.  (mdist(d;x;xs  i)  \mleq{}  (r1/r((2  *  (k  +  1))  +  1)))  BY
                          (ParallelOp  -2  THEN  RWO  "m-TB-iff"  (-1)  THEN  Auto))
  THEN  ((Skolemize  (-1)  `sz'  THENA  Auto)  THEN  Thin  (-3))
  THEN  (Skolemize  (-1)  `pts'  THENA  Auto)
  THEN  Thin  (-3))

---

Home Index