---

Step * 1 of Lemma path-end-mem-basic


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
BY
{ Assert ⌜∀g:Point(X ⟶ ℝ). ∀r:ℝ.  ((g(f@r1) < r) ⇒ (∃z:{z:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| t ∈ [z, r1]} . (g(f@t) < r)))⌝⋅ \000C}

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

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

---

Latex:

---

Latex:

1.  X  :  SeparationSpace
2.  f  :  Point(Path(X))
3.  B  :  ss-basic(X)
4.  f@r1  \mmember{}  B
\mvdash{}  \mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\}  .  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [z,  r1]\}  .  f@t  \mmember{}  B


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}g:Point(X  {}\mrightarrow{}  \mBbbR{}).  \mforall{}r:\mBbbR{}.
                    ((g(f@r1)  <  r)  {}\mRightarrow{}  (\mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\}  .  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [z,  r1]\}  .  (g(f@t)  <  r)))\mkleeneclose{}\mcdot{}

---

Home Index