---

Step * 2 1 of Lemma punctured-homeomorphism

.....assertion..... 
1. X : Type
2. Y : Type
3. d : metric(X)
4. d' : metric(Y)
5. mcomplete(X with d)
6. mcomplete(Y with d')
7. f : X ⟶ Y
8. f:FUN(X;Y)
9. g : Y ⟶ X
10. g:FUN(Y;X)
11. ∀x:X. g (f x) ≡ x
12. ∀y:Y. f (g y) ≡ y
13. p : Y
14. f ∈ {x:X| x # g p}  ⟶ {y:Y| y # p} 
⊢ g ∈ {y:Y| y # p}  ⟶ {x:X| x # g p} 
BY
{ ((FunExt THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN (InstLemma `msfun-ext-mfun` [⌜X⌝;⌜Y⌝;⌜d⌝;⌜d'⌝]⋅ THENA Auto)
   THEN (Assert f ∈ FUN(X ⟶ Y) BY
               (MemTypeCD THEN Auto))
   THEN (Assert f ∈ msfun(X;d;Y;d') BY
               (D -2 THEN Auto))
   THEN (MemTypeHD  (-1) THENA Auto)
   THEN (Unhide THENA Auto)
   THEN UnfoldTopAb (-1)
   THEN BHyp -1
   THEN Auto
   THEN RWO "12" 0⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  Type
2.  Y  :  Type
3.  d  :  metric(X)
4.  d'  :  metric(Y)
5.  mcomplete(X  with  d)
6.  mcomplete(Y  with  d')
7.  f  :  X  {}\mrightarrow{}  Y
8.  f:FUN(X;Y)
9.  g  :  Y  {}\mrightarrow{}  X
10.  g:FUN(Y;X)
11.  \mforall{}x:X.  g  (f  x)  \mequiv{}  x
12.  \mforall{}y:Y.  f  (g  y)  \mequiv{}  y
13.  p  :  Y
14.  f  \mmember{}  \{x:X|  x  \#  g  p\}    {}\mrightarrow{}  \{y:Y|  y  \#  p\} 
\mvdash{}  g  \mmember{}  \{y:Y|  y  \#  p\}    {}\mrightarrow{}  \{x:X|  x  \#  g  p\} 


By

---

Latex:
((FunExt  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  (InstLemma  `msfun-ext-mfun`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  f  \mmember{}  FUN(X  {}\mrightarrow{}  Y)  BY
                          (MemTypeCD  THEN  Auto))
  THEN  (Assert  f  \mmember{}  msfun(X;d;Y;d')  BY
                          (D  -2  THEN  Auto))
  THEN  (MemTypeHD    (-1)  THENA  Auto)
  THEN  (Unhide  THENA  Auto)
  THEN  UnfoldTopAb  (-1)
  THEN  BHyp  -1
  THEN  Auto
  THEN  RWO  "12"  0\mcdot{}
  THEN  Auto)

---

Home Index