---

Step * of Lemma homeomorphic_transitivity

∀[X,Y,Z:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)]. ∀[dZ:metric(Z)].
  (homeomorphic(X;dX;Y;dY) ⇒ homeomorphic(Y;dY;Z;dZ) ⇒ homeomorphic(X;dX;Z;dZ))
BY
{ (Auto
   THEN All (Unfold `homeomorphic`)
   THEN ExRepD
   THEN (D 0 With ⌜f o f1⌝  THENA (Try (BLemma  `compose-mfun`) THEN Auto))
   THEN (D 0 With ⌜g1 o g⌝  THENA (Try (BLemma  `compose-mfun`) THEN Auto))
   THEN (Subst' (g1 o g) o (f o f1) ~ g1 o ((g o f) o f1) 0 THENA (RepUR ``compose`` 0 THEN Auto))
   THEN (Subst' (f o f1) o (g1 o g) ~ f o ((f1 o g1) o g) 0 THENA (RepUR ``compose`` 0 THEN Auto))
   THEN RepUR ``compose`` 0
   THEN Auto) }

1
1. X : Type
2. Y : Type
3. Z : Type
4. dX : metric(X)
5. dY : metric(Y)
6. dZ : metric(Z)
7. f1 : FUN(X ⟶ Y)
8. g1 : FUN(Y ⟶ X)
9. ∀x:X. g1 (f1 x) ≡ x
10. ∀y:Y. f1 (g1 y) ≡ y
11. f : FUN(Y ⟶ Z)
12. g : FUN(Z ⟶ Y)
13. ∀x:Y. g (f x) ≡ x
14. ∀y:Z. f (g y) ≡ y
15. x : X
⊢ g1 (g (f (f1 x))) ≡ x

2
1. X : Type
2. Y : Type
3. Z : Type
4. dX : metric(X)
5. dY : metric(Y)
6. dZ : metric(Z)
7. f1 : FUN(X ⟶ Y)
8. g1 : FUN(Y ⟶ X)
9. ∀x:X. g1 (f1 x) ≡ x
10. ∀y:Y. f1 (g1 y) ≡ y
11. f : FUN(Y ⟶ Z)
12. g : FUN(Z ⟶ Y)
13. ∀x:Y. g (f x) ≡ x
14. ∀y:Z. f (g y) ≡ y
15. ∀x:X. g1 (g (f (f1 x))) ≡ x
16. y : Z
⊢ f (f1 (g1 (g y))) ≡ y

---

Latex:

---

Latex:
\mforall{}[X,Y,Z:Type].  \mforall{}[dX:metric(X)].  \mforall{}[dY:metric(Y)].  \mforall{}[dZ:metric(Z)].
    (homeomorphic(X;dX;Y;dY)  {}\mRightarrow{}  homeomorphic(Y;dY;Z;dZ)  {}\mRightarrow{}  homeomorphic(X;dX;Z;dZ))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `homeomorphic`)
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}f  o  f1\mkleeneclose{}    THENA  (Try  (BLemma    `compose-mfun`)  THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}g1  o  g\mkleeneclose{}    THENA  (Try  (BLemma    `compose-mfun`)  THEN  Auto))
  THEN  (Subst'  (g1  o  g)  o  (f  o  f1)  \msim{}  g1  o  ((g  o  f)  o  f1)  0  THENA  (RepUR  ``compose``  0  THEN  Auto))
  THEN  (Subst'  (f  o  f1)  o  (g1  o  g)  \msim{}  f  o  ((f1  o  g1)  o  g)  0  THENA  (RepUR  ``compose``  0  THEN  Auto))
  THEN  RepUR  ``compose``  0
  THEN  Auto)

---

Home Index