---

Step * 1 of Lemma mcompact-finite-subcover

.....aux..... 
1. [X] : Type
2. d : metric(X)
3. mcompact(X;d)
4. [I] : Type
5. [A] : I ⟶ X ⟶ ℙ
6. ∀i:I. m-open(X;d;x.A[i;x])
7. b : X ⟶ ℕ+
8. c : X ⟶ I
9. ∀x,y:X.  ((mdist(d;x;y) ≤ (r1/r(b x))) ⇒ A[c x;y])
10. cmplt : mcomplete(X with d)
11. mtb : m-TB(X;d)
12. B : ℕ
13. ∀x:X. ∃y:X. (x ≡ y ∧ (|b y| ≤ B))
⊢ ∃c:X ⟶ I. ∃B:ℕ. ∀x,y:X.  ((mdist(d;x;y) ≤ (r1/r(B + 1))) ⇒ A[c x;y])
BY
{ ((Skolemize (-1) `z' THENA Auto)
   THEN (InstConcl [⌜λx.(c (z x))⌝;⌜B⌝]⋅ THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN BackThruSomeHyp) }

1
1. [X] : Type
2. d : metric(X)
3. mcompact(X;d)
4. [I] : Type
5. [A] : I ⟶ X ⟶ ℙ
6. ∀i:I. m-open(X;d;x.A[i;x])
7. b : X ⟶ ℕ+
8. c : X ⟶ I
9. ∀x,y:X.  ((mdist(d;x;y) ≤ (r1/r(b x))) ⇒ A[c x;y])
10. cmplt : mcomplete(X with d)
11. mtb : m-TB(X;d)
12. B : ℕ
13. ∀x:X. ∃y:X. (x ≡ y ∧ (|b y| ≤ B))
14. z : x:X ⟶ X
15. ∀x:X. (x ≡ z x ∧ (|b (z x)| ≤ B))
16. x : X
17. y : X
18. mdist(d;x;y) ≤ (r1/r(B + 1))
⊢ mdist(d;z x;y) ≤ (r1/r(b (z x)))

---

Latex:

---

Latex:
.....aux..... 
1.  [X]  :  Type
2.  d  :  metric(X)
3.  mcompact(X;d)
4.  [I]  :  Type
5.  [A]  :  I  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}i:I.  m-open(X;d;x.A[i;x])
7.  b  :  X  {}\mrightarrow{}  \mBbbN{}\msupplus{}
8.  c  :  X  {}\mrightarrow{}  I
9.  \mforall{}x,y:X.    ((mdist(d;x;y)  \mleq{}  (r1/r(b  x)))  {}\mRightarrow{}  A[c  x;y])
10.  cmplt  :  mcomplete(X  with  d)
11.  mtb  :  m-TB(X;d)
12.  B  :  \mBbbN{}
13.  \mforall{}x:X.  \mexists{}y:X.  (x  \mequiv{}  y  \mwedge{}  (|b  y|  \mleq{}  B))
\mvdash{}  \mexists{}c:X  {}\mrightarrow{}  I.  \mexists{}B:\mBbbN{}.  \mforall{}x,y:X.    ((mdist(d;x;y)  \mleq{}  (r1/r(B  +  1)))  {}\mRightarrow{}  A[c  x;y])


By

---

Latex:
((Skolemize  (-1)  `z'  THENA  Auto)
  THEN  (InstConcl  [\mkleeneopen{}\mlambda{}x.(c  (z  x))\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  BackThruSomeHyp)

---

Home Index