Step * 1 of Lemma path-comp-property_functionality


1. [X] SeparationSpace
2. [Y] SeparationSpace
3. ss-homeo(X;Y)
4. ∀f,g:Point(Path(X)).  (f@r1 ≡ g@r0  (∃h:Point(Path(X)). path-comp-rel(X;f;g;h)))
5. Point(Path(Y))
6. Point(Path(Y))
7. f@r1 ≡ g@r0
⊢ ∃h:Point(Path(Y)). path-comp-rel(Y;f;g;h)
BY
(D THEN ExRepD) }

1
1. [X] SeparationSpace
2. [Y] SeparationSpace
3. f1 Point(X ⟶ Y)
4. g1 Point(Y ⟶ X)
5. ∀x:Point(X). g1(f1(x)) ≡ x
6. ∀y:Point(Y). f1(g1(y)) ≡ y
7. ∀f,g:Point(Path(X)).  (f@r1 ≡ g@r0  (∃h:Point(Path(X)). path-comp-rel(X;f;g;h)))
8. Point(Path(Y))
9. Point(Path(Y))
10. f@r1 ≡ g@r0
⊢ ∃h:Point(Path(Y)). path-comp-rel(Y;f;g;h)


Latex:


Latex:

1.  [X]  :  SeparationSpace
2.  [Y]  :  SeparationSpace
3.  ss-homeo(X;Y)
4.  \mforall{}f,g:Point(Path(X)).    (f@r1  \mequiv{}  g@r0  {}\mRightarrow{}  (\mexists{}h:Point(Path(X)).  path-comp-rel(X;f;g;h)))
5.  f  :  Point(Path(Y))
6.  g  :  Point(Path(Y))
7.  f@r1  \mequiv{}  g@r0
\mvdash{}  \mexists{}h:Point(Path(Y)).  path-comp-rel(Y;f;g;h)


By


Latex:
(D  3  THEN  ExRepD)




Home Index