---

Step * 2 1 1 1 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. Y : Type
10. d' : metric(Y)
11. f : X ⟶ Y
12. f:FUN(X;Y)
13. g : Y ⟶ X
14. ∀x1,x2:Y.  (x1 ≡ x2 ⇒ g[x1] ≡ g[x2])
15. ∀x:X. g (f x) ≡ x
16. ∀y:Y. f (g y) ≡ y
17. <f, g> ∈ homeomorphic(X;d;Y;d')
18. λy.(f (r (g y))) ∈ Y ⟶ homeo-image(A;Y;d';<f, g>)
19. λy.(f (r (g y))):FUN(Y;homeo-image(A;Y;d';<f, g>))
20. a : Y
21. b : A
22. a ≡ f b
23. g[a] ≡ g[f b]
⊢ g a ≡ b
BY
{ (RepUR ``so_apply`` -1 THEN (Assert b ∈ X BY Auto) THEN RWO "-2" 0 THEN Auto) }

---

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.  Y  :  Type
10.  d'  :  metric(Y)
11.  f  :  X  {}\mrightarrow{}  Y
12.  f:FUN(X;Y)
13.  g  :  Y  {}\mrightarrow{}  X
14.  \mforall{}x1,x2:Y.    (x1  \mequiv{}  x2  {}\mRightarrow{}  g[x1]  \mequiv{}  g[x2])
15.  \mforall{}x:X.  g  (f  x)  \mequiv{}  x
16.  \mforall{}y:Y.  f  (g  y)  \mequiv{}  y
17.  <f,  g>  \mmember{}  homeomorphic(X;d;Y;d')
18.  \mlambda{}y.(f  (r  (g  y)))  \mmember{}  Y  {}\mrightarrow{}  homeo-image(A;Y;d';<f,  g>)
19.  \mlambda{}y.(f  (r  (g  y))):FUN(Y;homeo-image(A;Y;d';<f,  g>))
20.  a  :  Y
21.  b  :  A
22.  a  \mequiv{}  f  b
23.  g[a]  \mequiv{}  g[f  b]
\mvdash{}  g  a  \mequiv{}  b


By

---

Latex:
(RepUR  ``so\_apply``  -1  THEN  (Assert  b  \mmember{}  X  BY  Auto)  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index