---

Step * of Lemma path-ss-point

No Annotations
∀[X:Top]
  (Point(Path(X)) ~ {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(X)| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t\000C')} )
BY
{ (RepUR ``path-ss ss-point ss-fun fun-ss set-ss mk-ss ss-function`` 0 THEN Fold `ss-point` 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Top]
    (Point(Path(X))  \msim{}  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(X)| 
                                          \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\}  )


By

---

Latex:
(RepUR  ``path-ss  ss-point  ss-fun  fun-ss  set-ss  mk-ss  ss-function``  0
  THEN  Fold  `ss-point`  0
  THEN  Auto)

---

Home Index