---

Step * 1 of Lemma punctured-homeomorphism


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} )
BY
{ (RepeatFor 2 (ParallelOp 8) THEN ParallelLast) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  2  (ParallelOp  8)  THEN  ParallelLast)

---

Home Index