---

Step * 1 of Lemma path-comp-set

.....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]}))
BY
{ ((All (RWW "path-ss-point set-ss-point set-ss-eq") THENA Auto) THEN D -2 THEN MemTypeCD THEN Auto) }

1
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:{f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(A)| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} .
     (f@r1 ≡ g@r0
     ⇒ (∃h:{f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(A)| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} 
          path-comp-rel(A;f;g;h)))
6. f : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ {a:Point(A)| P[a]} | ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')\000C} 
7. g : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ {a:Point(A)| P[a]} | ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')\000C} 
8. f@r1 ≡ g@r0
9. {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ {a:Point(A)| P[a]} | ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} 
     ⊆r {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(A)| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} 
10. h : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(A)
11. ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ h t ≡ h t')
12. path-comp-rel(A;f;g;h)
⊢ h ∈ {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ {a:Point(A)| P[a]} 

---

Latex:

---

Latex:
.....assertion..... 
1.  [A]  :  SeparationSpace
2.  [P]  :  Point(A)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a:Point(A).  Stable\{P[a]\}
4.  \mforall{}a,b:Point(A).    (a  \mequiv{}  b  {}\mRightarrow{}  P[b]  {}\mRightarrow{}  P[a])
5.  \mforall{}f,g:Point(Path(A)).    (f@r1  \mequiv{}  g@r0  {}\mRightarrow{}  (\mexists{}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  \mequiv{}  g@r0
9.  Point(Path(\{a:A  |  P[a]\}))  \msubseteq{}r  Point(Path(A))
10.  h  :  Point(Path(A))
11.  path-comp-rel(A;f;g;h)
\mvdash{}  h  \mmember{}  Point(Path(\{a:A  |  P[a]\}))


By

---

Latex:
((All  (RWW  "path-ss-point  set-ss-point  set-ss-eq")  THENA  Auto)  THEN  D  -2  THEN  MemTypeCD  THEN  Auto)

---

Home Index