---

Step * of Lemma homeo-image-inverse

No Annotations
∀[X,Y:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)]. ∀[h:homeomorphic(X;dX;Y;dY)]. ∀[A:Type].
  homeo-image(homeo-image(A;Y;dY;h);X;dX;homeo-inv(h)) ≡ A supposing metric-subspace(X;dX;A)
BY
{ (Auto
   THEN D -1
   THEN (RWO "strong-subtype-iff-respects-equality" (-2) THENA Auto)
   THEN D -2
   THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
.....subterm..... T:t
1:n
1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. h : homeomorphic(X;dX;Y;dY)
6. A : Type
7. A ⊆r X
8. respects-equality(X;A)
9. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
10. x : homeo-image(homeo-image(A;Y;dY;h);X;dX;homeo-inv(h))
⊢ x ∈ A

2
.....subterm..... T:t
1:n
1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. h : homeomorphic(X;dX;Y;dY)
6. A : Type
7. A ⊆r X
8. respects-equality(X;A)
9. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
10. x : A
⊢ x ∈ homeo-image(homeo-image(A;Y;dY;h);X;dX;homeo-inv(h))

---

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


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  (RWO  "strong-subtype-iff-respects-equality"  (-2)  THENA  Auto)
  THEN  D  -2
  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index