---

Step * 2 2 2 of Lemma punctured-homeomorphism

.....set predicate..... 
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} 
15. g ∈ {y:Y| y # p}  ⟶ {x:X| x # g p} 
⊢ g:FUN({y:Y| y # p} ;{x:X| x # g p} )
BY
{ (Thin (-1) THEN (GenConcl ⌜(g p) = a ∈ X⌝⋅ THENA Auto) THEN RepeatFor 2 (ParallelOp 10) THEN ParallelLast) }

---

Latex:

---

Latex:
.....set  predicate..... 
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\} 
15.  g  \mmember{}  \{y:Y|  y  \#  p\}    {}\mrightarrow{}  \{x:X|  x  \#  g  p\} 
\mvdash{}  g:FUN(\{y:Y|  y  \#  p\}  ;\{x:X|  x  \#  g  p\}  )


By

---

Latex:
(Thin  (-1)
  THEN  (GenConcl  \mkleeneopen{}(g  p)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelOp  10)
  THEN  ParallelLast)

---

Home Index