---

Step * of Lemma homeo-inv_wf

No Annotations
∀[X,Y:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)]. ∀[h:homeomorphic(X;dX;Y;dY)].  (homeo-inv(h) ∈ homeomorphic(Y;dY;X;dX))
BY
{ (Intros THEN Unhide THEN RepeatFor 2 (D -1) THEN RepUR ``homeo-inv homeomorphic exists sq_exists`` 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  RepeatFor  2  (D  -1)
  THEN  RepUR  ``homeo-inv  homeomorphic  exists  sq\_exists``  0
  THEN  Auto)

---

Home Index