---

Step * of Lemma punctured-homeomorphism

No Annotations
∀[X,Y:Type]. ∀[d:metric(X)]. ∀[d':metric(Y)].
  (mcomplete(X with d)
  ⇒ mcomplete(Y with d')
  ⇒ (∀h:homeomorphic(X;d;Y;d'). ∀p:Y.  (h ∈ homeomorphic({x:X| x # (snd(h)) p} ;d;{y:Y| y # p} ;d'))))
BY
{ (Auto
   THEN RepeatFor 2 (D -2)
   THEN RenameVar `g' (-3)
   THEN Reduce 0
   THEN (Assert f ∈ {x:X| x # g p}  ⟶ {y:Y| y # p}  BY
               ((FunExt THENA Auto)
                THEN D -1
                THEN MemTypeCD
                THEN Auto
                THEN (InstLemma `msfun-ext-mfun` [⌜Y⌝;⌜X⌝;⌜d'⌝;⌜d⌝]⋅ THENA Auto)
                THEN (Assert g ∈ msfun(Y;d';X;d) BY
                            (D -1 THEN Auto))
                THEN (MemTypeHD  (-1) THENA Auto)
                THEN (Unhide THENA Auto)
                THEN UnfoldTopAb (-1)
                THEN BHyp -1
                THEN Auto
                THEN RWO "9" 0⋅
                THEN Auto))
   THEN RepUR ``homeomorphic exists sq_exists`` 0
   THEN (MemCD THENA Auto)
   THEN DVar `f'
   THEN DVar `g'
   THEN MemTypeCD
   THEN Auto) }

1
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} 
⊢ f:FUN({x:X| x # g p} ;{y:Y| y # p} )

2
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 ∈ FUN({y:Y| y # p}  ⟶ {x:X| x # g p} )

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:Type].  \mforall{}[d:metric(X)].  \mforall{}[d':metric(Y)].
    (mcomplete(X  with  d)
    {}\mRightarrow{}  mcomplete(Y  with  d')
    {}\mRightarrow{}  (\mforall{}h:homeomorphic(X;d;Y;d').  \mforall{}p:Y.    (h  \mmember{}  homeomorphic(\{x:X|  x  \#  (snd(h))  p\}  ;d;\{y:Y|  y  \#  p\}  ;d')\000C)))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -2)
  THEN  RenameVar  `g'  (-3)
  THEN  Reduce  0
  THEN  (Assert  f  \mmember{}  \{x:X|  x  \#  g  p\}    {}\mrightarrow{}  \{y:Y|  y  \#  p\}    BY
                          ((FunExt  THENA  Auto)
                            THEN  D  -1
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  (InstLemma  `msfun-ext-mfun`  [\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (Assert  g  \mmember{}  msfun(Y;d';X;d)  BY
                                                    (D  -1  THEN  Auto))
                            THEN  (MemTypeHD    (-1)  THENA  Auto)
                            THEN  (Unhide  THENA  Auto)
                            THEN  UnfoldTopAb  (-1)
                            THEN  BHyp  -1
                            THEN  Auto
                            THEN  RWO  "9"  0\mcdot{}
                            THEN  Auto))
  THEN  RepUR  ``homeomorphic  exists  sq\_exists``  0
  THEN  (MemCD  THENA  Auto)
  THEN  DVar  `f'
  THEN  DVar  `g'
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index