---

Step * of Lemma homeomorphic_functionality

No Annotations
∀[X,Y,X',Y':Type].
  (∀[dX:metric(X)]. ∀[dY:metric(Y)].  homeomorphic(X;dX;Y;dY) ≡ homeomorphic(X';dX;Y';dY)) supposing (X ≡ X' and Y ≡ Y')
BY
{ (Unfold `ext-eq` 0
   THEN Intros
   THEN D 0
   THEN (Unhide THENA Auto)
   THEN ExRepD
   THEN (D 0 THENA Auto)
   THEN RepUR ``homeomorphic exists sq_exists`` 0
   THEN RepeatFor 2 (D -1)
   THEN D -3
   THEN D -2
   THEN (MemCD THENA Auto)
   THEN MemTypeCD
   THEN Auto
   THEN ((RepeatFor 2 (ParallelOp -5) THEN ParallelLast)
   ORELSE (MemTypeCD THEN Auto THEN RepeatFor 2 (ParallelOp -3) THEN ParallelLast)
   )) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y,X',Y':Type].
    (\mforall{}[dX:metric(X)].  \mforall{}[dY:metric(Y)].
          homeomorphic(X;dX;Y;dY)  \mequiv{}  homeomorphic(X';dX;Y';dY))  supposing 
          (X  \mequiv{}  X'  and 
          Y  \mequiv{}  Y')


By

---

Latex:
(Unfold  `ext-eq`  0
  THEN  Intros
  THEN  D  0
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``homeomorphic  exists  sq\_exists``  0
  THEN  RepeatFor  2  (D  -1)
  THEN  D  -3
  THEN  D  -2
  THEN  (MemCD  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  ((RepeatFor  2  (ParallelOp  -5)  THEN  ParallelLast)
  ORELSE  (MemTypeCD  THEN  Auto  THEN  RepeatFor  2  (ParallelOp  -3)  THEN  ParallelLast)
  ))

---

Home Index