---

Step * of Lemma path-at_wf

No Annotations
∀[X:SeparationSpace]. ∀[p:Point(Path(X))]. ∀[t:{t:ℝ| t ∈ [r0, r1]} ].  (p@t ∈ Point(X))
BY
{ (Auto THEN (RWO "path-ss-point" 2 THENA Auto) THEN ProveWfLemma) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (RWO  "path-ss-point"  2  THENA  Auto)  THEN  ProveWfLemma)

---

Home Index