---

Step * 1 1 of Lemma path-comp-set


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]} 
BY
{ (FunExt THENA 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)
13. x : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
⊢ h x ∈ {a:Point(A)| P[a]} 

---

Latex:

---

Latex:

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:\{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(A)| 
                  \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\}  .
          (f@r1  \mequiv{}  g@r0
          {}\mRightarrow{}  (\mexists{}h:\{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(A)| 
                          \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\} 
                    path-comp-rel(A;f;g;h)))
6.  f  :  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  \{a:Point(A)|  P[a]\}  | 
                \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\} 
7.  g  :  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  \{a:Point(A)|  P[a]\}  | 
                \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\} 
8.  f@r1  \mequiv{}  g@r0
9.  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  \{a:Point(A)|  P[a]\}  | 
        \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\} 
          \msubseteq{}r  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(A)| 
                  \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\} 
10.  h  :  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(A)
11.  \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  h  t  \mequiv{}  h  t')
12.  path-comp-rel(A;f;g;h)
\mvdash{}  h  \mmember{}  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  \{a:Point(A)|  P[a]\} 


By

---

Latex:
(FunExt  THENA  Auto)

---

Home Index