---

Step * 1 1 2 1 of Lemma mcomplete-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. ∀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. ∀i:T. ∃n:ℕ+. ∀a:{x:X| P[i;x]} . ((r1/r(n)) ≤ mdist(d;y;a))
13. n : ℕ+
14. ∀i:T. ∀a:{x:X| P[i;x]} .  ((r1/r(n)) ≤ mdist(d;y;a))
15. N : ℕ
16. ∀n@0:ℕ. ((N ≤ n@0) ⇒ (mdist(d;x n@0;y) ≤ (r1/r(n + 1))))
17. v : X
18. ∃i:T. P[i;v]
19. mdist(d;v;y) ≤ (r1/r(n + 1))
⊢ False
BY
{ (D -2 THEN (InstHyp [⌜i⌝;⌜v⌝] 14⋅ THENA 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. ∀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. ∀i:T. ∃n:ℕ+. ∀a:{x:X| P[i;x]} . ((r1/r(n)) ≤ mdist(d;y;a))
13. n : ℕ+
14. ∀i:T. ∀a:{x:X| P[i;x]} .  ((r1/r(n)) ≤ mdist(d;y;a))
15. N : ℕ
16. ∀n@0:ℕ. ((N ≤ n@0) ⇒ (mdist(d;x n@0;y) ≤ (r1/r(n + 1))))
17. v : X
18. i : T
19. P[i;v]
20. mdist(d;v;y) ≤ (r1/r(n + 1))
21. (r1/r(n)) ≤ mdist(d;y;v)
⊢ False

---

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.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  (mcauchy(d;n.x  n)  {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})
8.  cmp  :  \mforall{}i:T.  mcompact(\{x:X|  P[i;x]\}  ;d)
9.  x  :  \mBbbN{}  {}\mrightarrow{}  stable-union(X;T;i,x.P[i;x])
10.  mcauchy(d;n.x  n)
11.  y  :  X
12.  \mforall{}i:T.  \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}a:\{x:X|  P[i;x]\}  .  ((r1/r(n))  \mleq{}  mdist(d;y;a))
13.  n  :  \mBbbN{}\msupplus{}
14.  \mforall{}i:T.  \mforall{}a:\{x:X|  P[i;x]\}  .    ((r1/r(n))  \mleq{}  mdist(d;y;a))
15.  N  :  \mBbbN{}
16.  \mforall{}n@0:\mBbbN{}.  ((N  \mleq{}  n@0)  {}\mRightarrow{}  (mdist(d;x  n@0;y)  \mleq{}  (r1/r(n  +  1))))
17.  v  :  X
18.  \mexists{}i:T.  P[i;v]
19.  mdist(d;v;y)  \mleq{}  (r1/r(n  +  1))
\mvdash{}  False


By

---

Latex:
(D  -2  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]  14\mcdot{}  THENA  Auto))

---

Home Index