---

Step * of Lemma mcomplete-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)) ⇒ mcomplete(stable-union(X;T;i,x.P[i;x]) with \000Cd) 
  supposing ∀i:T. ∀x,y:X.  (P[i;x] ⇒ y ≡ x ⇒ P[i;y])
BY
{ (Auto
   THEN All (RepUR ``mcomplete``)
   THEN ParallelOp -2
   THEN RepeatFor 3 (ParallelLast)
   THEN MemTypeCD
   THEN Auto
   THEN RenameVar `cmp' 8
   THEN (InstLemma `not-not-finite-all-or-exists` [⌜T⌝;⌜λ2i.r0 < dist(y;{x:X| P[i;x]} )⌝]⋅ THENA Auto)
   THEN (SupposeMore (-1) THENA Auto)
   THEN D -1) }

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. ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
8. cmp : ∀i:T. mcompact({x:X| P[i;x]} ;d)
9. x : ℕ ⟶ stable-union(X;T;i,x.P[i;x])
10. mcauchy(d;n.x n)
11. y : X
12. lim n→∞.x n = y
13. ∀i:T. (r0 < dist(y;{x:X| P[i;x]} ))
⊢ ¬¬(∃i:T. P[i;y])

2
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. ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
8. cmp : ∀i:T. mcompact({x:X| P[i;x]} ;d)
9. x : ℕ ⟶ stable-union(X;T;i,x.P[i;x])
10. mcauchy(d;n.x n)
11. y : X
12. lim n→∞.x n = y
13. ∃i:T. (¬(r0 < dist(y;{x:X| P[i;x]} )))
⊢ ¬¬(∃i:T. P[i;y])

---

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


By

---

Latex:
(Auto
  THEN  All  (RepUR  ``mcomplete``)
  THEN  ParallelOp  -2
  THEN  RepeatFor  3  (ParallelLast)
  THEN  MemTypeCD
  THEN  Auto
  THEN  RenameVar  `cmp'  8
  THEN  (InstLemma  `not-not-finite-all-or-exists`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.r0  <  dist(y;\{x:X|  P[i;x]\}  )\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (SupposeMore  (-1)  THENA  Auto)
  THEN  D  -1)

---

Home Index