---

Step * of Lemma path-comp-set

No Annotations
∀[A:SeparationSpace]. ∀[P:Point(A) ⟶ ℙ].
  ((∀a:Point(A). Stable{P[a]})
  ⇒ (∀a,b:Point(A).  (a ≡ b ⇒ P[b] ⇒ P[a]))
  ⇒ path-comp-property(A)
  ⇒ path-comp-property({a:A | P[a]}))
BY
{ (Auto
   THEN All (Unfold `path-comp-property`)
   THEN Intros
   THEN (Assert Point(Path({a:A | P[a]})) ⊆r Point(Path(A)) BY
               ((D 0 THENA Auto)
                THEN (All (RWW "path-ss-point set-ss-point set-ss-eq") THENA Auto)
                THEN (D -1 THEN MemTypeCD)
                THEN Auto))
   THEN (InstHyp [⌜f⌝;⌜g⌝] 5⋅ THENA Auto)
   THEN D -1
   THEN (Assert ⌜h ∈ Point(Path({a:A | P[a]}))⌝⋅
   THENM ((D 0 With ⌜h⌝  THEN Auto) THEN RepeatFor 3 (ParallelOp -2) THEN Auto)
   )) }

1
.....assertion..... 
1. [A] : SeparationSpace
2. [P] : Point(A) ⟶ ℙ
3. ∀a:Point(A). Stable{P[a]}
4. ∀a,b:Point(A).  (a ≡ b ⇒ P[b] ⇒ P[a])
5. ∀f,g:Point(Path(A)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(A)). path-comp-rel(A;f;g;h)))
6. f : Point(Path({a:A | P[a]}))
7. g : Point(Path({a:A | P[a]}))
8. f@r1 ≡ g@r0
9. Point(Path({a:A | P[a]})) ⊆r Point(Path(A))
10. h : Point(Path(A))
11. path-comp-rel(A;f;g;h)
⊢ h ∈ Point(Path({a:A | P[a]}))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:SeparationSpace].  \mforall{}[P:Point(A)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a:Point(A).  Stable\{P[a]\})
    {}\mRightarrow{}  (\mforall{}a,b:Point(A).    (a  \mequiv{}  b  {}\mRightarrow{}  P[b]  {}\mRightarrow{}  P[a]))
    {}\mRightarrow{}  path-comp-property(A)
    {}\mRightarrow{}  path-comp-property(\{a:A  |  P[a]\}))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `path-comp-property`)
  THEN  Intros
  THEN  (Assert  Point(Path(\{a:A  |  P[a]\}))  \msubseteq{}r  Point(Path(A))  BY
                          ((D  0  THENA  Auto)
                            THEN  (All  (RWW  "path-ss-point  set-ss-point  set-ss-eq")  THENA  Auto)
                            THEN  (D  -1  THEN  MemTypeCD)
                            THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (Assert  \mkleeneopen{}h  \mmember{}  Point(Path(\{a:A  |  P[a]\}))\mkleeneclose{}\mcdot{}
  THENM  ((D  0  With  \mkleeneopen{}h\mkleeneclose{}    THEN  Auto)  THEN  RepeatFor  3  (ParallelOp  -2)  THEN  Auto)
  ))

---

Home Index