---

Step * of Lemma homeo-image-homeomorphic

No Annotations
∀[X,Y:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)].
  ∀h:homeomorphic(X;dX;Y;dY). ∀[A:Type]. homeomorphic(A;dX;homeo-image(A;Y;dY;h);dY) supposing metric-subspace(X;dX;A)
BY
{ (InstLemma `homeo-image-homeomorphic-subtype` [] THEN RepeatFor 7 (ParallelLast') THEN UseWitness ⌜h⌝⋅ THEN Trivial) }

---

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].  homeomorphic(A;dX;homeo-image(A;Y;dY;h);dY)  supposing  metric-subspace(X;dX;A)


By

---

Latex:
(InstLemma  `homeo-image-homeomorphic-subtype`  []
  THEN  RepeatFor  7  (ParallelLast')
  THEN  UseWitness  \mkleeneopen{}h\mkleeneclose{}\mcdot{}
  THEN  Trivial)

---

Home Index