---

Step * of Lemma homeo-image-boundary

No Annotations
∀[X,Y:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)].
  ∀h:homeomorphic(X;dX;Y;dY)
    ∀[A:Type]
      homeo-image(m-boundary(X;dX;A);Y;dY;h) ≡ m-boundary(Y;dY;homeo-image(A;Y;dY;h)) supposing metric-subspace(X;dX;A) 
    supposing PtwiseCONT(fst(h):X ⟶ Y) ∧ PtwiseCONT(snd(h):Y ⟶ X)
BY
{ (Auto
   THEN DupHyp (-1)
   THEN D -1
   THEN (RWO "strong-subtype-iff-respects-equality" (-2) THENA Auto)
   THEN (Assert h ∈ homeomorphic(X;dX;Y;dY) BY
               Declaration)
   THEN DVar `h'
   THEN DVar `h1'
   THEN (RepeatFor 2 (D 0) THENA (Auto THEN Reduce 0 THEN Auto))
   THEN D -1
   THEN ((DVar `x' THEN Reduce -2 THEN D -2) ORELSE (D -1 THEN Reduce -1 THEN DVar `a'))
   THEN (MemTypeCD THEN Auto)
   THEN Reduce 0
   THEN Auto
   THEN Try ((MemTypeCD THEN Reduce 0 THEN Auto))) }

1
1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. f : FUN(X ⟶ Y)
6. h1 : FUN(Y ⟶ X)
7. ∀x:X. h1 (f x) ≡ x
8. ∀y:Y. f (h1 y) ≡ y
9. PtwiseCONT(fst(<f, h1>):X ⟶ Y)
10. PtwiseCONT(snd(<f, h1>):Y ⟶ X)
11. A : Type
12. metric-subspace(X;dX;A)
13. A ⊆r X
14. respects-equality(X;A)
15. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
16. <f, h1> ∈ homeomorphic(X;dX;Y;dY)
17. x : Y
18. a : A
19. ¬m-interior-point(X;dX;A;a)
20. x ≡ f a
⊢ ¬m-interior-point(Y;dY;homeo-image(A;Y;dY;<f, h1>);x)

2
1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. f : FUN(X ⟶ Y)
6. h1 : FUN(Y ⟶ X)
7. ∀x:X. h1 (f x) ≡ x
8. ∀y:Y. f (h1 y) ≡ y
9. PtwiseCONT(fst(<f, h1>):X ⟶ Y)
10. PtwiseCONT(snd(<f, h1>):Y ⟶ X)
11. A : Type
12. metric-subspace(X;dX;A)
13. A ⊆r X
14. respects-equality(X;A)
15. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
16. <f, h1> ∈ homeomorphic(X;dX;Y;dY)
17. x : Y
18. a : A
19. x ≡ f a
20. ¬m-interior-point(Y;dY;homeo-image(A;Y;dY;<f, h1>);x)
⊢ ∃a:m-boundary(X;dX;A). x ≡ f a

---

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(m-boundary(X;dX;A);Y;dY;h)  \mequiv{}  m-boundary(Y;dY;homeo-image(A;Y;dY;h)) 
            supposing  metric-subspace(X;dX;A) 
        supposing  PtwiseCONT(fst(h):X  {}\mrightarrow{}  Y)  \mwedge{}  PtwiseCONT(snd(h):Y  {}\mrightarrow{}  X)


By

---

Latex:
(Auto
  THEN  DupHyp  (-1)
  THEN  D  -1
  THEN  (RWO  "strong-subtype-iff-respects-equality"  (-2)  THENA  Auto)
  THEN  (Assert  h  \mmember{}  homeomorphic(X;dX;Y;dY)  BY
                          Declaration)
  THEN  DVar  `h'
  THEN  DVar  `h1'
  THEN  (RepeatFor  2  (D  0)  THENA  (Auto  THEN  Reduce  0  THEN  Auto))
  THEN  D  -1
  THEN  ((DVar  `x'  THEN  Reduce  -2  THEN  D  -2)  ORELSE  (D  -1  THEN  Reduce  -1  THEN  DVar  `a'))
  THEN  (MemTypeCD  THEN  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((MemTypeCD  THEN  Reduce  0  THEN  Auto)))

---

Home Index