---

Step * of Lemma path-end-mem-basic

No Annotations
∀X:SeparationSpace. ∀f:Point(Path(X)). ∀B:ss-basic(X).
  (f@r1 ∈ B ⇒ (∃z:{z:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| t ∈ [z, r1]} . f@t ∈ B))
BY
{ Auto }

1
1. X : SeparationSpace
2. f : Point(Path(X))
3. B : ss-basic(X)
4. f@r1 ∈ B
⊢ ∃z:{z:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| t ∈ [z, r1]} . f@t ∈ B

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:SeparationSpace.  \mforall{}f:Point(Path(X)).  \mforall{}B:ss-basic(X).
    (f@r1  \mmember{}  B  {}\mRightarrow{}  (\mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\}  .  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [z,  r1]\}  .  f@t  \mmember{}  B))


By

---

Latex:
Auto

---

Home Index