---

Step * of Lemma path-comp-property_functionality

No Annotations
∀[X,Y:SeparationSpace].  (ss-homeo(X;Y) ⇒ (path-comp-property(X) ⇐⇒ path-comp-property(Y)))
BY
{ ((Assert ⌜∀[X,Y:SeparationSpace].  (ss-homeo(X;Y) ⇒ path-comp-property(X) ⇒ path-comp-property(Y))⌝⋅
   THENM (Auto THEN InstHyp [⌜Y⌝;⌜X⌝] 1⋅ THEN EAuto 1)
   )
   THEN Auto
   THEN ParallelLast
   THEN Auto) }

1
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. f : Point(Path(Y))
6. g : Point(Path(Y))
7. f@r1 ≡ g@r0
⊢ ∃h:Point(Path(Y)). path-comp-rel(Y;f;g;h)

---

Latex:

---

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


By

---

Latex:
((Assert 
    \mkleeneopen{}\mforall{}[X,Y:SeparationSpace].    (ss-homeo(X;Y)  {}\mRightarrow{}  path-comp-property(X)  {}\mRightarrow{}  path-comp-property(Y))\mkleeneclose{}\mcdot{}
  THENM  (Auto  THEN  InstHyp  [\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]  1\mcdot{}  THEN  EAuto  1)
  )
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto)

---

Home Index