---

Step * 1 of Lemma path-at_functionality


1. X : SeparationSpace
2. p : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(X)
3. ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ p t ≡ p t')
4. t : {t:ℝ| t ∈ [r0, r1]} 
5. t' : {t:ℝ| t ∈ [r0, r1]} 
6. t = t'
⊢ t ≡ t'
BY
{ EAuto 1 }

---

Latex:

---

Latex:

1.  X  :  SeparationSpace
2.  p  :  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(X)
3.  \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  p  t  \mequiv{}  p  t')
4.  t  :  \{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\} 
5.  t'  :  \{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\} 
6.  t  =  t'
\mvdash{}  t  \mequiv{}  t'


By

---

Latex:
EAuto  1

---

Home Index