---

Step * 1 of Lemma homeomorphic_transitivity


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
BY
{ ((D -3 With ⌜f1 x⌝  THENA Auto)
   THEN DVar `g1'
   THEN (Unhide THENA Auto)
   THEN ∀h:hyp. (RepUR ``is-mfun`` h THEN FHyp h [-1] THEN Auto) 
   THEN RepUR ``so_apply`` -1
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

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  {}\mrightarrow{}  Y)
8.  g1  :  FUN(Y  {}\mrightarrow{}  X)
9.  \mforall{}x:X.  g1  (f1  x)  \mequiv{}  x
10.  \mforall{}y:Y.  f1  (g1  y)  \mequiv{}  y
11.  f  :  FUN(Y  {}\mrightarrow{}  Z)
12.  g  :  FUN(Z  {}\mrightarrow{}  Y)
13.  \mforall{}x:Y.  g  (f  x)  \mequiv{}  x
14.  \mforall{}y:Z.  f  (g  y)  \mequiv{}  y
15.  x  :  X
\mvdash{}  g1  (g  (f  (f1  x)))  \mequiv{}  x


By

---

Latex:
((D  -3  With  \mkleeneopen{}f1  x\mkleeneclose{}    THENA  Auto)
  THEN  DVar  `g1'
  THEN  (Unhide  THENA  Auto)
  THEN  \mforall{}h:hyp.  (RepUR  ``is-mfun``  h  THEN  FHyp  h  [-1]  THEN  Auto) 
  THEN  RepUR  ``so\_apply``  -1
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index