---

Step * of Lemma ss-homotopic_inversion

No Annotations
∀X:SeparationSpace. ∀[x0,x1:Point(X)].  ∀a,b:Point(Path(X)).  (ss-homotopic(X;x0;x1;a;b) ⇒ ss-homotopic(X;x0;x1;b;a))
BY
{ (Auto
   THEN ParallelLast
   THEN ExRepD
   THEN (Assert λt.p@r1 - t ∈ Point(Path(Path(X))) BY
               ((RWO "path-ss-point" 0 THENA Auto)
                THEN MemTypeCD
                THEN Reduce 0
                THEN Auto
                THEN BLemma `path-at_functionality`
                THEN Auto
                THEN RWO "unit-ss-eq<" (-1)
                THEN Auto))
   THEN D 0 With ⌜λt.p@r1 - t⌝ 
   THEN Auto
   THEN RepUR ``path-at`` 0
   THEN Fold `path-at` 0
   THEN Try (RepeatFor 2 ((nRNorm 0 THEN Auto THEN MemTypeCD THEN Auto)))) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:SeparationSpace
    \mforall{}[x0,x1:Point(X)].    \mforall{}a,b:Point(Path(X)).    (ss-homotopic(X;x0;x1;a;b)  {}\mRightarrow{}  ss-homotopic(X;x0;x1;b;a))


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  ExRepD
  THEN  (Assert  \mlambda{}t.p@r1  -  t  \mmember{}  Point(Path(Path(X)))  BY
                          ((RWO  "path-ss-point"  0  THENA  Auto)
                            THEN  MemTypeCD
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  BLemma  `path-at\_functionality`
                            THEN  Auto
                            THEN  RWO  "unit-ss-eq<"  (-1)
                            THEN  Auto))
  THEN  D  0  With  \mkleeneopen{}\mlambda{}t.p@r1  -  t\mkleeneclose{} 
  THEN  Auto
  THEN  RepUR  ``path-at``  0
  THEN  Fold  `path-at`  0
  THEN  Try  (RepeatFor  2  ((nRNorm  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto))))

---

Home Index