---

Step * 1 1 of Lemma mcompact-finite-subcover


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)))
BY
{ ((D -4 With ⌜x⌝  THENA Auto)
   THEN D -1
   THEN (RWO "-2<" 0  THENA Auto)
   THEN (RWO "absval_pos" (-1) THENA Auto)
   THEN RWO "-3" 0
   THEN Auto) }

---

Latex:

---

Latex:

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))
14.  z  :  x:X  {}\mrightarrow{}  X
15.  \mforall{}x:X.  (x  \mequiv{}  z  x  \mwedge{}  (|b  (z  x)|  \mleq{}  B))
16.  x  :  X
17.  y  :  X
18.  mdist(d;x;y)  \mleq{}  (r1/r(B  +  1))
\mvdash{}  mdist(d;z  x;y)  \mleq{}  (r1/r(b  (z  x)))


By

---

Latex:
((D  -4  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  (RWO  "-2<"  0    THENA  Auto)
  THEN  (RWO  "absval\_pos"  (-1)  THENA  Auto)
  THEN  RWO  "-3"  0
  THEN  Auto)

---

Home Index