---

Step * 1 1 of Lemma homeo-image-homeomorphic-subtype


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>))
15. g ∈ homeo-image(A;Y;dY;<f, g>) ⟶ A
⊢ g ∈ FUN(homeo-image(A;Y;dY;<f, g>) ⟶ A)
BY
{ (DVar `g' THEN MemTypeCD THEN Auto THEN RepeatFor 2 (ParallelOp 7) THEN ParallelLast) }

---

Latex:

---

Latex:

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


By

---

Latex:
(DVar  `g'  THEN  MemTypeCD  THEN  Auto  THEN  RepeatFor  2  (ParallelOp  7)  THEN  ParallelLast)

---

Home Index