---

Step * of Lemma homeomorphic-retraction

No Annotations
∀[X,A:Type]. ∀[d:metric(X)].
  Retract(X ⟶ A) ⇒ (∀Y:Type. ∀d':metric(Y). ∀h:homeomorphic(X;d;Y;d').  Retract(Y ⟶ homeo-image(A;Y;d';h))) 
  supposing metric-subspace(X;d;A)
BY
{ ((Auto THEN (Assert h ∈ homeomorphic(X;d;Y;d') BY Declaration))
   THEN D 4
   THEN (RWO "strong-subtype-iff-respects-equality" 4 THENA Auto)
   THEN D 6
   THEN RepeatFor 2 (D -2)
   THEN RenameVar `r' 6
   THEN RenameVar `f' (-4)
   THEN RenameVar `g' (-3)
   THEN (Assert λy.(f (r (g y))) ∈ Y ⟶ homeo-image(A;Y;d';<f, g>) BY
               (DVar `g'
                THEN DVar `f'
                THEN (MemCD THENA Auto)
                THEN MemTypeCD
                THEN Auto
                THEN Reduce 0
                THEN Try (D 0 With ⌜r (g y)⌝ )
                THEN Auto))
   THEN D 0 With ⌜λy.(f (r (g y)))⌝ 
   THEN Reduce 0
   THEN Auto) }

1
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>)
⊢ λy.(f (r (g y))):FUN(Y;homeo-image(A;Y;d';<f, g>))

2
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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,A:Type].  \mforall{}[d:metric(X)].
    Retract(X  {}\mrightarrow{}  A)
    {}\mRightarrow{}  (\mforall{}Y:Type.  \mforall{}d':metric(Y).  \mforall{}h:homeomorphic(X;d;Y;d').    Retract(Y  {}\mrightarrow{}  homeo-image(A;Y;d';h))) 
    supposing  metric-subspace(X;d;A)


By

---

Latex:
((Auto  THEN  (Assert  h  \mmember{}  homeomorphic(X;d;Y;d')  BY  Declaration))
  THEN  D  4
  THEN  (RWO  "strong-subtype-iff-respects-equality"  4  THENA  Auto)
  THEN  D  6
  THEN  RepeatFor  2  (D  -2)
  THEN  RenameVar  `r'  6
  THEN  RenameVar  `f'  (-4)
  THEN  RenameVar  `g'  (-3)
  THEN  (Assert  \mlambda{}y.(f  (r  (g  y)))  \mmember{}  Y  {}\mrightarrow{}  homeo-image(A;Y;d';<f,  g>)  BY
                          (DVar  `g'
                            THEN  DVar  `f'
                            THEN  (MemCD  THENA  Auto)
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  Reduce  0
                            THEN  Try  (D  0  With  \mkleeneopen{}r  (g  y)\mkleeneclose{}  )
                            THEN  Auto))
  THEN  D  0  With  \mkleeneopen{}\mlambda{}y.(f  (r  (g  y)))\mkleeneclose{} 
  THEN  Reduce  0
  THEN  Auto)

---

Home Index