---

Step * 2 of Lemma homeomorphic-retraction


1. X : Type
2. A : Type
3. d : metric(X)
4. A ⊆r X
5. respects-equality(X;A)
6. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
7. r : X ⟶ A
8. r:FUN(X;A)
9. ∀a:A. r a ≡ a
10. Y : Type
11. d' : metric(Y)
12. f : FUN(X ⟶ Y)
13. g : FUN(Y ⟶ X)
14. ∀x:X. g (f x) ≡ x
15. ∀y:Y. f (g y) ≡ y
16. <f, g> ∈ homeomorphic(X;d;Y;d')
17. λy.(f (r (g y))) ∈ Y ⟶ homeo-image(A;Y;d';<f, g>)
18. λy.(f (r (g y))):FUN(Y;homeo-image(A;Y;d';<f, g>))
19. a : homeo-image(A;Y;d';<f, g>)
⊢ f (r (g a)) ≡ a
BY
{ (DVar `f'
   THEN D -1
   THEN Reduce -1
   THEN (Unhide THENA Auto)
   THEN D -1
   THEN RenameVar `b' (-2)
   THEN (D 9 With ⌜g a⌝ 
   THENM (UnfoldTopAb (-11) THEN (FHyp (-11) [-1] THENA Auto) THEN RepUR ``so_apply`` -1 THEN RWO "15" (-1) THEN Auto)
   )) }

1
.....wf..... 
1. X : Type
2. A : Type
3. d : metric(X)
4. A ⊆r X
5. respects-equality(X;A)
6. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
7. r : X ⟶ A
8. r:FUN(X;A)
9. Y : Type
10. d' : metric(Y)
11. f : X ⟶ Y
12. f:FUN(X;Y)
13. g : FUN(Y ⟶ X)
14. ∀x:X. g (f x) ≡ x
15. ∀y:Y. f (g y) ≡ y
16. <f, g> ∈ homeomorphic(X;d;Y;d')
17. λy.(f (r (g y))) ∈ Y ⟶ homeo-image(A;Y;d';<f, g>)
18. λy.(f (r (g y))):FUN(Y;homeo-image(A;Y;d';<f, g>))
19. a : Y
20. b : A
21. a ≡ f b
⊢ g a ∈ A

---

Latex:

---

Latex:

1.  X  :  Type
2.  A  :  Type
3.  d  :  metric(X)
4.  A  \msubseteq{}r  X
5.  respects-equality(X;A)
6.  \mforall{}a:A.  \mforall{}x:X.    (x  \mequiv{}  a  {}\mRightarrow{}  (x  \mmember{}  A))
7.  r  :  X  {}\mrightarrow{}  A
8.  r:FUN(X;A)
9.  \mforall{}a:A.  r  a  \mequiv{}  a
10.  Y  :  Type
11.  d'  :  metric(Y)
12.  f  :  FUN(X  {}\mrightarrow{}  Y)
13.  g  :  FUN(Y  {}\mrightarrow{}  X)
14.  \mforall{}x:X.  g  (f  x)  \mequiv{}  x
15.  \mforall{}y:Y.  f  (g  y)  \mequiv{}  y
16.  <f,  g>  \mmember{}  homeomorphic(X;d;Y;d')
17.  \mlambda{}y.(f  (r  (g  y)))  \mmember{}  Y  {}\mrightarrow{}  homeo-image(A;Y;d';<f,  g>)
18.  \mlambda{}y.(f  (r  (g  y))):FUN(Y;homeo-image(A;Y;d';<f,  g>))
19.  a  :  homeo-image(A;Y;d';<f,  g>)
\mvdash{}  f  (r  (g  a))  \mequiv{}  a


By

---

Latex:
(DVar  `f'
  THEN  D  -1
  THEN  Reduce  -1
  THEN  (Unhide  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `b'  (-2)
  THEN  (D  9  With  \mkleeneopen{}g  a\mkleeneclose{} 
  THENM  (UnfoldTopAb  (-11)
                THEN  (FHyp  (-11)  [-1]  THENA  Auto)
                THEN  RepUR  ``so\_apply``  -1
                THEN  RWO  "15"  (-1)
                THEN  Auto)
  ))

---

Home Index