---

Step * of Lemma path-at_functionality2

No Annotations
∀[X:SeparationSpace]. ∀[p:Point(Path(X))]. ∀[t,t':{t:ℝ| t ∈ [r0, r1]} ].  p@t ≡ p@t' supposing t ≡ t'
BY
{ Auto }

1
1. X : SeparationSpace
2. p : Point(Path(X))
3. t : {t:ℝ| t ∈ [r0, r1]} 
4. t' : {t:ℝ| t ∈ [r0, r1]} 
5. t ≡ t'
⊢ p@t ≡ p@t'

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:SeparationSpace].  \mforall{}[p:Point(Path(X))].  \mforall{}[t,t':\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  ].    p@t  \mequiv{}  p@t'  supposing  t  \mequiv{}  t\000C'


By

---

Latex:
Auto

---

Home Index