---

Step * of Lemma ss-homeo_transitivity

No Annotations
∀[X,Y,Z:SeparationSpace].  (ss-homeo(X;Y) ⇒ ss-homeo(Y;Z) ⇒ ss-homeo(X;Z))
BY
{ (Auto
   THEN All (Unfold `ss-homeo`)
   THEN ExRepD
   THEN (D 0 With ⌜ss-comp(f;f1)⌝  THENA Auto)
   THEN (D 0 With ⌜ss-comp(g1;g)⌝  THENA Auto)) }

1
1. [X] : SeparationSpace
2. [Y] : SeparationSpace
3. [Z] : SeparationSpace
4. f1 : Point(X ⟶ Y)@i
5. g1 : Point(Y ⟶ X)@i
6. ∀x:Point(X). g1(f1(x)) ≡ x
7. ∀y:Point(Y). f1(g1(y)) ≡ y
8. f : Point(Y ⟶ Z)@i
9. g : Point(Z ⟶ Y)@i
10. ∀x:Point(Y). g(f(x)) ≡ x
11. ∀y:Point(Z). f(g(y)) ≡ y
⊢ (∀x:Point(X). ss-comp(g1;g)(ss-comp(f;f1)(x)) ≡ x) ∧ (∀y:Point(Z). ss-comp(f;f1)(ss-comp(g1;g)(y)) ≡ y)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y,Z:SeparationSpace].    (ss-homeo(X;Y)  {}\mRightarrow{}  ss-homeo(Y;Z)  {}\mRightarrow{}  ss-homeo(X;Z))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `ss-homeo`)
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}ss-comp(f;f1)\mkleeneclose{}    THENA  Auto)
  THEN  (D  0  With  \mkleeneopen{}ss-comp(g1;g)\mkleeneclose{}    THENA  Auto))

---

Home Index