---

Step * of Lemma ss-homotopic_weakening

No Annotations
∀X:SeparationSpace
  ∀[x0,x1:Point(X)].  ∀a,b:Point(Path(X)).  (ss-homotopic(X;x0;x1;a;b)) supposing (a ≡ b and b@r0 ≡ x0 and b@r1 ≡ x1)
BY
{ (Auto
   THEN (Assert λt.b ∈ Point(Path(Path(X))) BY
               (RWO "path-ss-point" 0 THEN Auto THEN MemTypeCD THEN Reduce 0 THEN Auto))
   ) }

1
1. X : SeparationSpace@i'
2. [x0] : Point(X)
3. [x1] : Point(X)
4. a : Point(Path(X))@i
5. b : Point(Path(X))@i
6. b@r1 ≡ x1
7. b@r0 ≡ x0
8. a ≡ b
9. λt.b ∈ Point(Path(Path(X)))
⊢ ss-homotopic(X;x0;x1;a;b)

---

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))  supposing  (a  \mequiv{}  b  and  b@r0  \mequiv{}  x0  and  b@r1  \mequiv{}  x1)


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}t.b  \mmember{}  Point(Path(Path(X)))  BY
                          (RWO  "path-ss-point"  0  THEN  Auto  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto))
  )

---

Home Index