---

Step * of Lemma ss-free-homotopic_inversion

No Annotations
∀X:SeparationSpace. ∀a,b:Point(X).  (ss-free-homotopic(X;a;b) ⇒ ss-free-homotopic(X;b;a))
BY
{ (Auto THEN ParallelLast THEN ExRepD THEN D 0 With ⌜λt.p@r1 - t⌝  THEN Auto) }

1
.....wf..... 
1. X : SeparationSpace@i'
2. a : Point(X)@i
3. b : Point(X)@i
4. p : Point(Path(X))@i
5. p@r0 ≡ a
6. p@r1 ≡ b
⊢ λt.p@r1 - t ∈ Point(Path(X))

2
1. X : SeparationSpace@i'
2. a : Point(X)@i
3. b : Point(X)@i
4. p : Point(Path(X))@i
5. p@r0 ≡ a
6. p@r1 ≡ b
⊢ λt.p@r1 - t@r0 ≡ b

3
1. X : SeparationSpace@i'
2. a : Point(X)@i
3. b : Point(X)@i
4. p : Point(Path(X))@i
5. p@r0 ≡ a
6. p@r1 ≡ b
7. λt.p@r1 - t@r0 ≡ b
⊢ λt.p@r1 - t@r1 ≡ a

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:SeparationSpace.  \mforall{}a,b:Point(X).    (ss-free-homotopic(X;a;b)  {}\mRightarrow{}  ss-free-homotopic(X;b;a))


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  ExRepD  THEN  D  0  With  \mkleeneopen{}\mlambda{}t.p@r1  -  t\mkleeneclose{}    THEN  Auto)

---

Home Index