---

Step * of Lemma homeo-image-homeomorphic-subtype

No Annotations
∀[X,Y:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)]. ∀[h:homeomorphic(X;dX;Y;dY)]. ∀[A:Type].
  h ∈ homeomorphic(A;dX;homeo-image(A;Y;dY;h);dY) supposing metric-subspace(X;dX;A)
BY
{ (Intros
   THEN Unhide
   THEN DupHyp (-1)
   THEN D -1
   THEN (RWO "strong-subtype-iff-respects-equality" (-2) THENA Auto)
   THEN (Assert h ∈ homeomorphic(X;dX;Y;dY) BY
               Declaration)
   THEN DVar `h'
   THEN DVar `h1'
   THEN RenameVar `g' 6
   THEN (Assert f ∈ A ⟶ homeo-image(A;Y;dY;<f, g>) BY
               ((FunExt THENW Auto) THEN MemTypeCD THEN Reduce 0 THEN Auto))
   THEN (Assert f ∈ FUN(A ⟶ homeo-image(A;Y;dY;<f, g>)) BY
               (DVar `f' THEN MemTypeCD THEN Try ((RepeatFor 2 (ParallelOp 6) THEN ParallelLast)) THEN Auto))
   THEN RepUR ``homeomorphic exists sq_exists`` 0
   THEN (MemCD THENA Auto)
   THEN Try (Trivial)
   THEN (MemTypeCD THENW Auto)
   THEN Try ((ParallelOp 7 THEN ParallelOp 8))) }

1
1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. f : FUN(X ⟶ Y)
6. g : FUN(Y ⟶ X)
7. (∀x:X. g (f x) ≡ x) ∧ (∀y:Y. f (g y) ≡ y)
8. A : Type
9. metric-subspace(X;dX;A)
10. (A ⊆r X) ∧ respects-equality(X;A)
11. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
12. <f, g> ∈ homeomorphic(X;dX;Y;dY)
13. f ∈ A ⟶ homeo-image(A;Y;dY;<f, g>)
14. f ∈ FUN(A ⟶ homeo-image(A;Y;dY;<f, g>))
⊢ g ∈ FUN(homeo-image(A;Y;dY;<f, g>) ⟶ A)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:Type].  \mforall{}[dX:metric(X)].  \mforall{}[dY:metric(Y)].  \mforall{}[h:homeomorphic(X;dX;Y;dY)].  \mforall{}[A:Type].
    h  \mmember{}  homeomorphic(A;dX;homeo-image(A;Y;dY;h);dY)  supposing  metric-subspace(X;dX;A)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  DupHyp  (-1)
  THEN  D  -1
  THEN  (RWO  "strong-subtype-iff-respects-equality"  (-2)  THENA  Auto)
  THEN  (Assert  h  \mmember{}  homeomorphic(X;dX;Y;dY)  BY
                          Declaration)
  THEN  DVar  `h'
  THEN  DVar  `h1'
  THEN  RenameVar  `g'  6
  THEN  (Assert  f  \mmember{}  A  {}\mrightarrow{}  homeo-image(A;Y;dY;<f,  g>)  BY
                          ((FunExt  THENW  Auto)  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto))
  THEN  (Assert  f  \mmember{}  FUN(A  {}\mrightarrow{}  homeo-image(A;Y;dY;<f,  g>))  BY
                          (DVar  `f'
                            THEN  MemTypeCD
                            THEN  Try  ((RepeatFor  2  (ParallelOp  6)  THEN  ParallelLast))
                            THEN  Auto))
  THEN  RepUR  ``homeomorphic  exists  sq\_exists``  0
  THEN  (MemCD  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  (MemTypeCD  THENW  Auto)
  THEN  Try  ((ParallelOp  7  THEN  ParallelOp  8)))

---

Home Index