---

Step * of Lemma mcompact_functionality_wrt_homeomorphic+

No Annotations
∀X,Y:Type. ∀d:metric(X). ∀d':metric(Y).  (homeomorphic+(Y;d';X;d) ⇒ mcompact(X;d) ⇒ mcompact(Y;d'))
BY
{ ((Auto THEN RepeatFor 3 (D -2) THEN D -4)
   THEN (InstLemma `compact-metric-to-metric-continuity` [⌜X⌝;⌜d⌝;⌜Y⌝;⌜d'⌝;⌜g⌝]⋅ THENA Auto)
   THEN ParallelOp -2
   THEN All (Fold `and`)
   THEN All (RWO "m-TB-iff")
   THEN Auto) }

1
1. X : Type
2. Y : Type
3. d : metric(X)
4. d' : metric(Y)
5. f : FUN(Y ⟶ X)
6. g : FUN(X ⟶ Y)
7. [%6] : (∀x:Y. g (f x) ≡ x) ∧ (∀y:X. f (g y) ≡ y)
8. B : ℕ+
9. [%5] : ∀x1,x2:Y.  (mdist(d;f x1;f x2) ≤ (r(B) * mdist(d';x1;x2)))
10. mcomplete(X with d)
11. ∀k:ℕ. ∃n:ℕ+. ∃xs:ℕn ⟶ X. ∀x:X. ∃i:ℕn. (mdist(d;x;xs i) ≤ (r1/r(k + 1)))
12. UC(g:X ⟶ Y)
⊢ mcomplete(Y with d')

2
1. X : Type
2. Y : Type
3. d : metric(X)
4. d' : metric(Y)
5. f : FUN(Y ⟶ X)
6. g : FUN(X ⟶ Y)
7. [%6] : (∀x:Y. g (f x) ≡ x) ∧ (∀y:X. f (g y) ≡ y)
8. B : ℕ+
9. [%5] : ∀x1,x2:Y.  (mdist(d;f x1;f x2) ≤ (r(B) * mdist(d';x1;x2)))
10. mcomplete(X with d)
11. ∀k:ℕ. ∃n:ℕ+. ∃xs:ℕn ⟶ X. ∀x:X. ∃i:ℕn. (mdist(d;x;xs i) ≤ (r1/r(k + 1)))
12. UC(g:X ⟶ Y)
13. mcomplete(Y with d')
14. k : ℕ
⊢ ∃n:ℕ+. ∃xs:ℕn ⟶ Y. ∀x:Y. ∃i:ℕn. (mdist(d';x;xs i) ≤ (r1/r(k + 1)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}X,Y:Type.  \mforall{}d:metric(X).  \mforall{}d':metric(Y).
    (homeomorphic+(Y;d';X;d)  {}\mRightarrow{}  mcompact(X;d)  {}\mRightarrow{}  mcompact(Y;d'))


By

---

Latex:
((Auto  THEN  RepeatFor  3  (D  -2)  THEN  D  -4)
  THEN  (InstLemma  `compact-metric-to-metric-continuity`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  All  (Fold  `and`)
  THEN  All  (RWO  "m-TB-iff")
  THEN  Auto)

---

Home Index